Agda can't find standard library modules

[mhwombat]

Issue description

Agda can't find standard library modules.

Steps to reproduce

1. Install haskellPackages.Agda and AgdaStdlib.

2. Create the following file called hello-world.agda.

module hello-world where

open import IO

main = run (putStrLn "Hello, World!")

3. At a shell prompt, type agda --compile hello-world.agda.

$ agda --compile hello-world.agda
Checking hello-world (/home/amy/néal/agda/hello-world.agda).
/home/amy/néal/agda/hello-world.agda:3,1-15
Failed to find source of module IO in any of the following
locations:
  /home/amy/néal/agda/IO.agda
  /home/amy/néal/agda/IO.lagda
  /nix/store/yrcgczibkkx3zgry8g44l9gamz0k87fh-Agda-2.6.0.1-data/share/ghc-8.6.5/x86_64-linux-ghc-8.6.5/Agda-2.6.0.1/lib/prim/IO.agda
  /nix/store/yrcgczibkkx3zgry8g44l9gamz0k87fh-Agda-2.6.0.1-data/share/ghc-8.6.5/x86_64-linux-ghc-8.6.5/Agda-2.6.0.1/lib/prim/IO.lagda
when scope checking the declaration
  open import IO

Technical details

$ nix-shell -p nix-info --run "nix-info -m"
warning: unknown setting 'system-features'
these paths will be fetched (0.11 MiB download, 0.45 MiB unpacked):
  /nix/store/61shjilahl0d237fg9b3z3chza2lgms4-patchelf-0.9
  /nix/store/67ddmyshs02nqkfs2sgyvq3wn0fgdpwa-bash-interactive-4.4-p23-dev
  /nix/store/bh0034wm3y1zrizdg3pcfx6h56lc7wk3-stdenv-linux
copying path '/nix/store/67ddmyshs02nqkfs2sgyvq3wn0fgdpwa-bash-interactive-4.4-p23-dev' from 'https://cache.nixos.org'...
copying path '/nix/store/61shjilahl0d237fg9b3z3chza2lgms4-patchelf-0.9' from 'https://cache.nixos.org'...
copying path '/nix/store/bh0034wm3y1zrizdg3pcfx6h56lc7wk3-stdenv-linux' from 'https://cache.nixos.org'...
warning: unknown setting 'system-features'
 - system: `"x86_64-linux"`
 - host os: `Linux 4.14.118, NixOS, 19.09pre181392.4ab1c14714f (Loris)`
 - multi-user?: `yes`
 - sandbox: `yes`
warning: unknown setting 'system-features'
 - version: `nix-env (Nix) 2.1.3`
warning: unknown setting 'system-features'
 - channels(amy): `"nixpkgs-18.09.1676.7e88992a8c7"`
warning: unknown setting 'system-features'                                                                                   
 - channels(root): `"nixos-19.09pre181392.4ab1c14714f"`                                                                      
warning: unknown setting 'system-features'                                                                                   
 - nixpkgs: `/nix/var/nix/profiles/per-user/root/channels/nixos`                                                             

Note: Possibly related to issue #19434.

[mhwombat]

More info:

$ sudo find / -name IO.agda
/nix/store/ljcr12pj1zspiyi4w5s421j8xx4h0wxh-agda-stdlib-1.0/share/agda/IO.agda
/nix/store/nkiqj8c08sa7x05vabig6m6bfj5sv731-Agda-2.5.4.1-data/share/ghc-8.4.4/x86_64-linux-ghc-8.4.4/Agda-2.5.4.1/lib/prim/Agda/Builtin/IO.agda
/nix/store/yrcgczibkkx3zgry8g44l9gamz0k87fh-Agda-2.6.0.1-data/share/ghc-8.6.5/x86_64-linux-ghc-8.6.5/Agda-2.6.0.1/lib/prim/Agda/Builtin/IO.agda

[alexarice]

I've had a little look into this and agda seems to be in a bit of a mess. I managed to get hello world to work with the following shell.nix

{ pkgs ? import ./nixpkgs {} }:

with pkgs;

let
  pkg = agda.mkDerivation(self: {
    name = "MyPackage";
    buildDepends = [ pkgs.AgdaStdlib (pkgs.haskellPackages.ghcWithPackages ( p: [p.ieee]) ) ];
  });
in
  pkg.env

I agree this really isn't ideal and it really wasn't obvious that my compile wasn't working due to missing ghc packages. Ideally a ghc with the correct packages loaded would be fed into agda. A agdaWithPackages as suggested in #39318 would also be nice although that pr seems to have not much happening / have problems I don't really understand about interactive mode and emacs.

Sorry if this wasn't much help

[mhwombat]

Thank you @alexarice , that's a good workaround.

[alexarice]

What needs to happen for this issue to be resolved?

[turion]

This somehow solves the issue for compilation. How do I use the standard library in interactive mode, though?

[turion]

FWIW, I found this helpful: http://blog.ielliott.io/agda-nixos/
It helped me get agda up and running interactively.

[alexarice]

you might also be able to use direnv

[bbarker]

Unfortunately I wasn't able to get any of the suggested workarounds here working myself. However, I was able to use agda-pkg in a nix-shell environment to get things running. Here's my template repository: https://github.com/bbarker/LearningAgda. I hope others might find it useful in the meantime, and any feedback you have is welcome.