Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Installation with nix #381

Closed
ju-sh opened this issue Dec 18, 2024 · 17 comments
Closed

Installation with nix #381

ju-sh opened this issue Dec 18, 2024 · 17 comments

Comments

@ju-sh
Copy link

ju-sh commented Dec 18, 2024

Hi.

Is agda2hs usable via nix out of the box?

I tried using the shell.nix with nix-shell.
Got these warnings but spotted no errors:

Warning: haddock-interfaces: /nix/store/wxw2713m8f0b8dmhin6f0357xsc5fcis-attoparsec-0.14.4/share/doc/x86_64-linux-ghc-9.6.5/attoparsec-0.14.4/html/attoparsec.haddock doesn't exist or isn't a file
Warning: haddock-html: /nix/store/wxw2713m8f0b8dmhin6f0357xsc5fcis-attoparsec-0.14.4/share/doc/x86_64-linux-ghc-9.6.5/attoparsec-0.14.4/html doesn't exist or isn't a directory
Warning: include-dirs: /nix/store/g6fy1axin55fmc6lwiv1lrvkij0ydppr-ghc-9.6.5-with-packages/lib/ghc-9.6.5/lib/../lib/x86_64-linux-ghc-9.6.5/directory-1.3.8.4/include doesn't exist or isn't a directory
Warning: haddock-interfaces: /nix/store/wxw2713m8f0b8dmhin6f0357xsc5fcis-attoparsec-0.14.4/share/doc/x86_64-linux-ghc-9.6.5/attoparsec-0.14.4/html/attoparsec.haddock doesn't exist or isn't a file
Warning: haddock-html: /nix/store/wxw2713m8f0b8dmhin6f0357xsc5fcis-attoparsec-0.14.4/share/doc/x86_64-linux-ghc-9.6.5/attoparsec-0.14.4/html doesn't exist or isn't a directory

But it didn't seem to work:

user@host:~/repos/agda2hs$ nix-shell

[nix-shell:~/repos/agda2hs]$ agda2hs
bash: agda2hs: command not found

Any idea how this can be fixed?

Thanks.

@jespercockx
Copy link
Member

I'm not a nix user myself but I know @liesnikov uses Agda2Hs with Nix so perhaps they can help.

@liesnikov
Copy link
Contributor

liesnikov commented Dec 18, 2024

I'm assuming you cloned the repo locally and ran nix shell in the directory? If so, this drops you in a shell to develop agda2hs, not to use it.
You can instantiate a shell with agda2hs available like this:

user@pc:~$ nix shell github:agda/agda2hs
[...download and compilation output...]
user@pc:~$ which agda2hs # it's available now
/nix/store/gbn5d084k4qk3hl9gb0k4z30d0ffsyxc-agda2hsWithPackages-1.3/bin/agda2hs

This just pulls the latest commit from github, so you don't have to clone the repo. You do have to enable flakes for this though.

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024 via email

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024 via email

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024 via email

@liesnikov
Copy link
Contributor

I tried to whip something up quickly to use without flakes, could you try using this package?

https://github.com/liesnikov/agda2hs/blob/master/nix/default.nix

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024

I cloned that repo and tried it like:

[nix-shell:~/repos/agda2hs]$ nix-shell nix/
copying path '/nix/store/dfr3hrqa2x7a3xxvn9wx8nxd488l027v-distribution-nixpkgs-1.7.1-data' from 'https://cache.nixos.org'...
copying path '/nix/store/22c9jcbyjywkxr49qrydcj3a921xsv79-stdenv-linux' from 'https://cache.nixos.org'...
copying path '/nix/store/4mj3vw66cgyhpxwprgi1k9vxbl7ql1r6-cabal2nix-2.19.1' from 'https://cache.nixos.org'...
building '/nix/store/vai79m9zv0b5mv3gs60rvmmkj3pcghzq-cabal2nix-agda2hs.drv'...
error: nix-shell requires a single derivation
Try 'nix-shell --help' for more information.

But I don't know what that error means, really..

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024

I am on 24.05 channel now, I think I need 24.11 for agda 2.7
Let me upgrade.

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024

No same error with 24.11 channel too.

But I kind of randomly tried: cd nix; nix-shell -A agda2hs default.nix.
It copied a bunch of stuff and dropped to a shell but agda2hs wasn't there in path.

@liesnikov
Copy link
Contributor

liesnikov commented Dec 18, 2024

I meant trying something like nix-shell -p "(import ./nix/default.nix {}).agda2hs". This should drop you in a shell with agda2hs available on path, built from your local sources and using your default <nixpkgs> channel.

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024

I meant trying something like nix-shell -p "(import ./nix/default.nix {}).agda2hs".

Oh.. 😅

built from your local sources and using your default <nixpkgs> channel.

Thanks! It worked.

$ agda2hs --version
Agda version 2.7.0.1
Built with flags (cabal -f)
 - optimise-heavily: extra optimisations
 - debug: enable debug printing ('-v' verbosity flags)
 - agda2hs backend version 1.3

But agda2hs locate isn't working.

$ agda2hs locate
/home/user/repos/agda2hs/locate:1,1-1
Cannot read file /home/user/repos/agda2hs/locate
Error: /home/user/repos/agda2hs/locate: openBinaryFile: does not exist (No such file or directory)

Is it that the part for that needs to be added onto one of the nix files?

@liesnikov
Copy link
Contributor

After a discussion with @flupe it seems that the locate doesn't work if it's not the very first argument.
When built with nix, agda2hs get wrapped to pass the libraries file explicitly, so locate isn't the first argument anymore.

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024

nix-shell -p "(import ./nix/default.nix {}).agda2hs" gave this:

Running phase: buildPhase
Preprocessing executable 'agda2hs' for agda2hs-1.3..
Building executable 'agda2hs' for agda2hs-1.3..
[ 1 of 23] Compiling Agda2Hs.HsUtils  ( src/Agda2Hs/HsUtils.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/HsUtils.o )
[ 2 of 23] Compiling Agda2Hs.Compile.Types ( src/Agda2Hs/Compile/Types.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Types.o )
[ 3 of 23] Compiling Agda2Hs.Compile.Var ( src/Agda2Hs/Compile/Var.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Var.o )
[ 4 of 23] Compiling Agda2Hs.Pragma   ( src/Agda2Hs/Pragma.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Pragma.o )
[ 5 of 23] Compiling AgdaInternals    ( src/AgdaInternals.hs, dist/build/agda2hs/agda2hs-tmp/AgdaInternals.o )
[ 6 of 23] Compiling Agda2Hs.AgdaUtils ( src/Agda2Hs/AgdaUtils.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/AgdaUtils.o )
[ 7 of 23] Compiling Agda2Hs.Compile.Utils ( src/Agda2Hs/Compile/Utils.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Utils.o )
[ 8 of 23] Compiling Agda2Hs.Compile.Name ( src/Agda2Hs/Compile/Name.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Name.o )
[ 9 of 23] Compiling Agda2Hs.Config   ( src/Agda2Hs/Config.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Config.o )
[10 of 23] Compiling Agda2Hs.Compile.Type ( src/Agda2Hs/Compile/Type.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Type.o )
[11 of 23] Compiling Agda2Hs.Compile.TypeDefinition ( src/Agda2Hs/Compile/TypeDefinition.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/TypeDefinition.o )
[12 of 23] Compiling Agda2Hs.Compile.Postulate ( src/Agda2Hs/Compile/Postulate.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Postulate.o )
[13 of 23] Compiling Agda2Hs.Compile.Data ( src/Agda2Hs/Compile/Data.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Data.o )
[14 of 23] Compiling Agda2Hs.Compile.Imports ( src/Agda2Hs/Compile/Imports.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Imports.o )
[15 of 23] Compiling Agda2Hs.Compile.Function[boot] ( src/Agda2Hs/Compile/Function.hs-boot, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Function.o-boot )
[16 of 23] Compiling Agda2Hs.Compile.Term ( src/Agda2Hs/Compile/Term.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Term.o )
[17 of 23] Compiling Agda2Hs.Compile.Function ( src/Agda2Hs/Compile/Function.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Function.o )
[18 of 23] Compiling Agda2Hs.Compile.ClassInstance ( src/Agda2Hs/Compile/ClassInstance.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/ClassInstance.o )
[19 of 23] Compiling Agda2Hs.Compile.Record ( src/Agda2Hs/Compile/Record.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile/Record.o )
[20 of 23] Compiling Agda2Hs.Compile  ( src/Agda2Hs/Compile.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Compile.o )
[21 of 23] Compiling Agda2Hs.Render   ( src/Agda2Hs/Render.hs, dist/build/agda2hs/agda2hs-tmp/Agda2Hs/Render.o )
[22 of 23] Compiling Paths_agda2hs    ( dist/build/agda2hs/autogen/Paths_agda2hs.hs, dist/build/agda2hs/agda2hs-tmp/Paths_agda2hs.o )
[23 of 23] Compiling Main             ( src/Main.hs, dist/build/agda2hs/agda2hs-tmp/Main.o )
[24 of 24] Linking dist/build/agda2hs/agda2hs
Running phase: checkPhase
Package has no test suites.
Running phase: haddockPhase
Running phase: installPhase
Installing executable agda2hs in /nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3/bin
Warning: The directory
/nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3/bin is not in the
system search path.
Running phase: fixupPhase
shrinking RPATHs of ELF executables and libraries in /nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3
shrinking /nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3/bin/agda2hs
checking for references to /build/ in /nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3...
patching script interpreter paths in /nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3
stripping (with command strip and flags -S -p) in  /nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3/bin
shrinking RPATHs of ELF executables and libraries in /nix/store/99bkrh0pcvz4nh1cxysn69ysqz4lhhhv-agda2hs-1.3-data
checking for references to /build/ in /nix/store/99bkrh0pcvz4nh1cxysn69ysqz4lhhhv-agda2hs-1.3-data...
patching script interpreter paths in /nix/store/99bkrh0pcvz4nh1cxysn69ysqz4lhhhv-agda2hs-1.3-data
shrinking RPATHs of ELF executables and libraries in /nix/store/fmx7k18lyhapjwysm6yss7cpqhgya8sh-agda2hs-1.3-doc
checking for references to /build/ in /nix/store/fmx7k18lyhapjwysm6yss7cpqhgya8sh-agda2hs-1.3-doc...
patching script interpreter paths in /nix/store/fmx7k18lyhapjwysm6yss7cpqhgya8sh-agda2hs-1.3-doc
building '/nix/store/dhgv61k3h6vnz31scgrcr04gz1gza9mc-agda2hsWithPackages-1.3.drv'...

But using the path directly works:

$ /nix/store/yzsijfwdx6z99b9bhv6hp4miklkmkaik-agda2hs-1.3/bin/agda2hs locate
/nix/store/99bkrh0pcvz4nh1cxysn69ysqz4lhhhv-agda2hs-1.3-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/agda2hs-1.3/agda2hs.agda-lib

@liesnikov
Copy link
Contributor

liesnikov commented Dec 18, 2024

locate expects to be the very first argument to agda2hs, this doesn't hold when we wrap agda2hs in a wrapper during the nix build. On top of that, I'm not sure how will this locate behave with nix, where the agda library is packaged separately, see #372 (comment).

So at the moment locate does not work with nix-distributed agda2hs.

@ju-sh
Copy link
Author

ju-sh commented Dec 18, 2024

I was trying the Test.agda file from here as a 'hello world' with agda2hs (With the module name filled in, just in case).

Got this error:

$ agda2hs Test.agda
Checking Test (/home/user/Test.agda).
/home/user/Test.agda:5,1-28
Failed to find source of module Haskell.Prelude in any of the
following locations:
  /home/user/Haskell/Prelude.agda
  /home/user/Haskell/Prelude.lagda
  /nix/store/5rrcjka802d69fmn69rizxg15av0x89l-Agda-2.7.0.1-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/Agda-2.7.0.1/lib/prim/Haskell/Prelude.agda
  /nix/store/5rrcjka802d69fmn69rizxg15av0x89l-Agda-2.7.0.1-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/Agda-2.7.0.1/lib/prim/Haskell/Prelude.lagda
when scope checking the declaration
  open import Haskell.Prelude

Could this error be circumvented?

I put this is ~/.agda/libraries:

/nix/store/99bkrh0pcvz4nh1cxysn69ysqz4lhhhv-agda2hs-1.3-data/share/ghc-9.6.6/x86_64-linux-ghc-9.6.6/agda2hs-1.3/agda2hs.agda-lib

Could it be because of the direct path to nix store?

@liesnikov
Copy link
Contributor

When using nix builds, agda2hs doesn't come with the prelude linked. I see four ways to circumvent this:

  1. Install agda2hs using cabal. I think something like nix-shell ./nix will work to install the dependencies?
  2. Start using flakes. If your concerns are with space perhaps you can pin nixpkgs to a different version?
  3. Use something like
    nix-shell -p "let packages = import ./nix/default.nix {}; lib = import ./nix/lib.nix {}; in (lib.withPackages [ packages.agda2hs-lib ])"
    
    If you want to link more libraries you can also look here or here for inspiration and recreate something similar without the flakes.
  4. Perhaps you can install agda2hs locally using nix and then manage all libraries (including or excluding agda2hs built-in one) by hand.

The problems you are experiencing are not really specific to agda2hs, but to nix and path management.
So, I'm afraid, this is not the right place to discuss it. If nix is causing you trouble perhaps building agda2hs with just ghcup and cabal will be easier.

@ju-sh
Copy link
Author

ju-sh commented Dec 20, 2024

I tried the first option. But had errors.
I opened a new issue for that at #386

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

3 participants