agda-categories: init at 0.1

[alexarice]

Motivation for this change

agda-categories was not part of nixpkgs.

Things done

• 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 nix-review --run "nix-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 @Fuuzetsu as I think you know what is going on with agda stuff.

Few notes on this:

• I had to patch the .agda-lib file to remove the dependency as otherwise it fails saying it cannot find it. This is due to the way the agda infrastructure is set up on nix I believe, it might be worth fixing this instead of hacking round it like I have done
• This took 18GB of ram to build, can hydra cope with that

[Fuuzetsu]

cc @Fuuzetsu as I think you know what is going on with agda stuff.

Haven't touched any of it for years, I think there were some improvements others have done on top of my initial version. If you need more eyes, git blame the Agda builder I think.

I had to patch the .agda-lib file to remove the dependency as otherwise it fails saying it cannot find it. This is due to the way the agda infrastructure is set up on nix I believe, it might be worth fixing this instead of hacking round it like I have done

The whole agda-lib system didn't exist back when I originally wrote the nix stuff. nix was actually the very first Agda package manager if you will. I think probably in the long run we should support it like we do with cabal for Haskell &c.

This took 18GB of ram to build, can hydra cope with that

🤷‍♂️ , I think you can mark it to not be built on Hydra but it might be fine.

[Fuuzetsu]

Perhaps AgdaStdLib is badly named so it can't detect it. Probably it'd not be too hard to figure out what this agda-lib stuff is looking for and make it so that AgdaStdLib dependency is picked up by it without changing this file.

[alexarice]

The problem is that the default for all the agda-lib stuff is ~/.agda which isn't a very convenient location for nix. I believe this can be modified by the AGDA_DIR environment variable so I might have a play around at some point if I have time. I wonder if wrapping agda to have this set to some nix generated folder would allow the agda builder to be simpler/ make an agdaWithPackages derivation very easy

[alexarice]

Have made a bigger pull request (#76653) which reworks the builder to use the agda-lib system. This PR includes this one so I am going to close this