bbarker / LearningAgda

Agda learning repo with some handy nix expressions
1 stars 0 forks source link

Unable to run #1

Open LaloHao opened 3 years ago

LaloHao commented 3 years ago

As promissed in the docs, bare Agda, fails to find the standard library

[hao@wendy:~/dev/agda]$ agda --compile hello-world.agda
Checking hello-world (/home/hao/dev/agda/hello-world.agda).
/home/hao/dev/agda/hello-world.agda:3,1-15
Failed to find source of module IO in any of the following
locations:
  /home/hao/dev/agda/IO.agda
  /home/hao/dev/agda/IO.lagda
  /nix/store/63rxng4xg4rsf1bjccmnj0l1bxqc6ab2-Agda-2.6.1-data/share/ghc-8.8.4/x86_64-linux-ghc-8.8.4/Agda-2.6.1/lib/prim/IO.agda
  /nix/store/63rxng4xg4rsf1bjccmnj0l1bxqc6ab2-Agda-2.6.1-data/share/ghc-8.8.4/x86_64-linux-ghc-8.8.4/Agda-2.6.1/lib/prim/IO.lagda
when scope checking the declaration
  open import IO

However using shell.nix also failed

[hao@wendy:~/dev/agda/LearningAgda]$ nix-shell
error: attribute 'mkDerivation' missing, at /home/hao/dev/agda/LearningAgda/shell.nix:7:1

I managed to solved it by changing the package call, even though i'm unsure if that's the right way of doing it

modified   deps.nix
@@ -2,7 +2,8 @@ with import <nixpkgs> {};
 let
   thisAgda = pkgs.haskellPackages.ghcWithPackages ( p: [p.Agda p.ieee754] );
 in
-agda.mkDerivation(self:  {
+agdaPackages.mkDerivation {
+  pname = "commonAgdaDeps";
   name = "commonAgdaDeps";
   dontUnpack = true;
   myAgda = thisAgda;
@@ -13,4 +14,4 @@ agda.mkDerivation(self:  {
     # pkgs.agdaPrelude (pkgs.haskellPackages.ghcWithPackages ( p: [p.ieee]) )
   ];
   src = null;
-})
+}
modified   shell.nix
@@ -2,9 +2,9 @@ with import <nixpkgs> {};
 let
   deps = (import ./deps.nix);
   myEmacs = (import ./emacs.nix { inherit pkgs; });
-  
 in
-agda.mkDerivation(self:  {
+agdaPackages.mkDerivation {
+  pname = "agdaShellEnv";
   name = "agdaShellEnv";
   dontUnpack = true;
   buildDepends = deps.buildDepends;
@@ -70,4 +70,4 @@ agda.mkDerivation(self:  {
       emacs -Q --load $AGDA_PROJ_DIR/.emacs $@
     }
   '';
-})
+}

I don't know anything about agda but that did seem to stop complaining about stdlib and managed to get a new error which i find great since that seems to be a regular ghc/nix problem

Compilation error:

MAlonzo/RTE.hs:9:1: error:
    Could not find module ‘Numeric.IEEE’
    Use -v (or `:set -v` in ghci) to see a list of the files searched for.
  |
9 | import Numeric.IEEE ( IEEE(identicalIEEE, nan) )
  | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Thanks for the repo

I'll check later to see if i can fix the missing library, i saw it in deps.nix, but for some reason it didn't load, i did ran emacs from inside nix-shell, however i use gccemacs (emacs 28), with spacemacs, that seems like a double problem

arjunv27 commented 3 years ago

Agda has been revamped for 20.09. Quite easy to use.