Agda rework

[alexarice]

Motivation for this change

• Current Agda infrastructure is 5 years old
• There are a lot of broken agda packages
• There is a lot of confusion on how to use the agda infrastructure (see: Agda can't find standard library modules #62546 , https://www.reddit.com/r/agda/comments/efjr39/agda_on_nixos/ )
• Agda has it's own library framework now
• Some agda packages have weird names

Fixes #60271
Fixes #62546

Things done

• Removed broken packages which have no hope of being fixed
• Remade the agda builder to use the new library infrastructure of Agda
• Made the current working agda packages work with this infrastructure
• Fixed agda-prelude so that it actually builds everything
• Renamed packages into an agda scope
• Added package agda-categories (this can be split into a separate PR but I wanted to check that agda packages with agda dependencies worked)

• Tested using sandboxing (nix.useSandbox on NixOS, or option sandbox in nix.conf on non-NixOS linux)
• Built on platform(s)
  • NixOS
  • macOS
  • other Linux distributions
• Tested via one or more NixOS test(s) if existing and applicable for the change (look inside nixos/tests)
• Tested compilation of all pkgs that depend on this change using nix-shell -p nixpkgs-review --run "nixpkgs-review wip"
• Tested execution of all binary files (usually in ./result/bin/)
• Determined the impact on package closure size (by running nix path-info -S before and after)
• Ensured that relevant documentation is up to date
• Fits CONTRIBUTING.md.

Notify maintainers

cc @jwiegley @laMudri

There should possibly be some documentation for this

[laMudri]

Thanks for putting the work in here. Given that my usual way of using Agda libraries totally bypassed Nix, it was clear that something had to be done. Furthermore, the Agda community could really benefit from some way to make builds reproducible, because with the language and standard library changing quickly, reproducing builds is often hard.

Before writing the documentation fully, could you give a quick overview of the intended workflow? In particular, I think it would be worth recommending something to deal with Emacs integration (I've never managed to do this with Haskell, for example).

I'm slightly concerned with the “compile everything and put it in /nix/store/” approach which (IIUC) this proposal sticks to. Compiling the standard library all in one go takes several gigabytes of RAM, which on some machines is a serious inconvenience. Other libraries can be worse (I imagine agda-categories is). Also, it makes things much more difficult for those using master versions or working on a library. All caching is lost, even when only a tiny change to the library is made. Do you have recommendations for either of these situations?

[alexarice]

Before writing the documentation fully, could you give a quick overview of the intended workflow? In particular, I think it would be worth recommending something to deal with Emacs integration (I've never managed to do this with Haskell, for example).

My workflow using this is to install say agda.agdaWithPackages (p: [ p.standard-library ]). This then has the effect of setting up the libraries file. Unfortunately at the moment there appears to be no nice way to write to defaults (it could be done by overriding the $AGDA_DIR environment variable. Therefore the user can either write their own or write an .agda-lib file for the directory they are working in.

I haven't tested it a lot yet, but with this workflow emacs integration seems to work out the box. If you wanted to get a version of agda from nix-shell, I think direnv and direnv-mode would be the easiest way to get this to work.

I'm slightly concerned with the “compile everything and put it in /nix/store/” approach which (IIUC) this proposal sticks to.

It does stick to this

Compiling the standard library all in one go takes several gigabytes of RAM, which on some machines is a serious inconvenience. Other libraries can be worse (I imagine agda-categories is).

This is why I have put hydraPlatforms = [] on agda-categories. It takes a lot of RAM (see agda/agda-categories#38)

Also, it makes things much more difficult for those using master versions or working on a library. All caching is lost, even when only a tiny change to the library is made. Do you have recommendations for either of these situations?

I think it could be hard to work round this issue. Some things I thought of:

• For master versions of libraries, it might be easiest to just not use the nixified agda, I can't see much of a way round this. It would be easier to use a mix of nix packages and non nix packages if Agda let you specify multiple library files (as then one could be in the home directory and one in the nix store)
• I don't know much about the internals of Agda so this could be wrong, but perhaps it would take less RAM to individually compile each file instead of compiling an Everything.agda file (It seems to me that Agda tries to store the whole library in memory when using the Everything.agda file)
• Perhaps it could be set up to not build the library, and Agda could be told to put the .agdai files somewhere in the home directory (I tried --compile-dir though this didn't seem to do anything so I'm not sure how this works).
• This would be a lot more work but I definitely saw a haskell thing which generated a separate nix derivation for each file and compiled them separately somehow. Not sure this would be suitable for nixpkgs though

[alexarice]

Have rebased to fix merge conflict

[Mic92]

Is this PR considered ready?

[alexarice]

Is this package considered ready?

I think not quite yet, could do with someone else to look through/test it I think + resolve the problems in the discussion above

[alexarice]

Changed to using makeWrapper
@GrahamcOfBorg build agda.standard-library agda.iowa-stdlib agda.agda-prelude

[laMudri]

Having thought about it a bit more, it makes sense to work on libraries in a non-Nixified state, so it's not too unreasonable to assume that this is what one should do to work with master-branch versions too.

Perhaps, though, it would be possible to do something cleverer. In cases where the Agda version stays the same, but the library changes, it should be the case that most .agdai files are still helpful. In particular, we may want to depend on an old, stable version of the library and copy its .agdai files over before building the new version. It feels like this could be done at a later time if it's really wanted, though, so I'll say that not doing it is fine.

perhaps it would take less RAM to individually compile each file

I think this would be nice as an option in the generic builder, which we would hope to deprecate if/when Agda becomes better at building libraries. Do something like: build each file individually, so as to yield .agdai files, then do the usual steps to build the Everything file. This should ensure some level of equivalence.

One more issue: how does this deal with compilation? If I remember correctly, compilation output can live in a different directory (--compile-dir?), and that's why it doesn't need to be done at package build time. If so, this should go in the documentation.

[alexarice]

The only way I can see of doing incremental builds is by generating a nix expression for each file, as in https://github.com/nmattia/snack, though I am not sure this sort of thing lives in nixpkgs and as you have said, if you need to rebuild a library a lot it may make more sense for it to be in your home directory.

I will try to add the building each file separately and seeing how it goes, the ways I can see of doing this are:

• grepping the Everything file for import statements
• running find in the directory for *.agda

I'm not sure which of these is preferable

I have actually never really tried to compile anything before, I'll give it a try.

One final thing, I believe that agda does not accept having multiple library files, would it be worth adding an option in agdaWithPackages to add extra lines to the generated library file (which could point to home directory libraries), I think it would be useful but doesn't seem very nixy

[alexarice]

Compiling works, it seems to put all the files in your working directory by default. This also acts on the .agdai files and seems to work very quickly (compared to the type checking)

[alexarice]

adding find . -name '*.agda' -and -not -name 'Everything.agda' -execdir agda {} + looks like it could be a cheap hack which fixes some memory issues

[laMudri]

stdlib also has files like EverythingSafe.agda, so this isn't going to work in general.

[alexarice]

I'm sure the bash can be improved but

grep 'import' Everything.agda | awk '{ print $2 }' | sed 's/\./\//g' | sed 's/$/\.agda/g' | xargs -i agda '{}'

?

[alexarice]

awk '/import/{ gsub(/\./,"/",$2); cmd = "agda "$2".agda"; system(cmd) }' Everything.agda

perhaps this is better (though more cryptic)

[laMudri]

Just spotted another thing: I never got round to reviewing #76217, but agda-stdlib should be at version 1.2. We might as well make that change in this PR to avoid conflicts.

[alexarice]

Just spotted another thing: I never got round to reviewing #76217, but agda-stdlib should be at version 1.2. We might as well make that change in this PR to avoid conflicts.

is 1.2 for agda verson 2.6.0.1?

[laMudri]

Yep

[alexarice]

Will add this in a sec, what else needs to be done?

[alexarice]

Have addressed discussions above

[veprbl]

I suggest we merge this as long as this evaluates/builds and take on further improvements in follow up PR's.

@GrahamcOfBorg build agda agdaPackages.standard-library
@GrahamcOfBorg test agda

[alexarice]

Seems to be fine on linux and for some reason tries to compile agda and times out on darwin and aarch64

[veprbl]

nixpkgs-review on x86_64-darwin:

2 package marked as broken and skipped:
agdaPackages.agda-prelude agdaPackages.iowa-stdlib

1 package built:
agdaPackages.standard-library

[veprbl]

Thank you @alexarice @chkno @laMudri @turion!

[turion]

I will ask on the Agda mailing list what typical libraries are that people use and try to bring them into this framework. My dream would be that nix/nixpkgs could be established as the quasi standard package manager for Agda.

[alexarice]

One issue is most libraries don't seem to be publishing a release when a new agda version comes out though I was just planning on pinning some commits for each so that they at least work

[turion]

One issue is most libraries don't seem to be publishing a release when a new agda version comes out though I was just planning on pinning some commits for each so that they at least work

You mean pinning an agda commit or a library commit?

Yeah, nixpkgs could play the role that stackage plays in the Haskell world. (Except that the Agda ecosystem a few orders of magnitude smaller.)

[turion]

One issue is most libraries don't seem to be publishing a release when a new agda version comes out though I was just planning on pinning some commits for each so that they at least work

You mean pinning an agda commit or a library commit?

Yeah, nixpkgs could play the role that stackage plays in the Haskell world. (Except that the Agda ecosystem a few orders of magnitude smaller.)

By that I mean that we can ping the library maintainers in a more systematic way, and point them to a reproducible failing build.