Agda cubical

[ryanorendorff]

Motivation for this change

Adds the cubical type theory library to nixpkgs. I asked the maintainers and @Saizan gave approval to add this library to 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) (checked for any tests, there do not appear to be).
• 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/) (all agda files compile)
• Determined the impact on package closure size (by running nix path-info -S before and after)
• Ensured that relevant documentation is up to date (I cannot find a place in the documentation for Agda things)
• Fits CONTRIBUTING.md.

Notify maintainers

cc @jwiegley @laMudri

[laMudri]

Possibly some modifications will be needed when #76653 is merged. /cc @alexarice

[alexarice]

This would need to be modified slightly, either this can be merged and I rebase on top of it or the other way round

[alexarice]

Might be easier to merge this first

[ryanorendorff]

Doesn't matter to me. I can also modify this if the other PR is merged first. @alexarice

[veprbl]

@ryanorendorff This will need to be adapted for the new Agda infrastructure. See manual https://github.com/NixOS/nixpkgs/blob/d30e2468e0c7875d3d4d47404f52647ccea76fcf/doc/languages-frameworks/agda.section.md

[alexarice]

Note that v0.1 won't compile with agda 2.6.1 and there is not a more recent version

[veprbl]

@alexarice This warrants getting more versions of Agda in nixpkgs?

[alexarice]

Perhaps, I feel the libraries should release a version that works with the new agda version, as the master versions of these libraries work

[ryanorendorff]

We could choose some development commit that passes their integration server for now.

…

On May 15, 2020, at 12:39, Alex Rice ***@***.***> wrote:  Perhaps, I feel the libraries should release a version that works with the new agda version, as the master versions of these libraries work — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

[alexarice]

I feel this is the sensible option

[ryanorendorff]

Ok I’ll find a good commit and update the PR when it builds correctly.

…

On May 15, 2020, at 12:47, Alex Rice ***@***.***> wrote:  I feel this is the sensible option — You are receiving this because you were mentioned. Reply to this email directly, view it on GitHub, or unsubscribe.

[Saizan]

I ended up tagging a recent master as the 0.2 release, it does work with 2.6.1:
https://github.com/agda/cubical/releases/tag/v0.2

[alexarice]

@Saizan I tried out that commit and get the following error:

these derivations will be built:
  /nix/store/1xsk4ln5yi13y5s0cn1i57ccl42nchj9-cubical-0.2.drv
building '/nix/store/1xsk4ln5yi13y5s0cn1i57ccl42nchj9-cubical-0.2.drv'...
unpacking sources
unpacking source archive /nix/store/r5mlcnbhcp77y5wn7xxhggyi1wsaqnas-source
source root is source
patching sources
configuring
no configure script, doing nothing
building
runhaskell ./Everythings.hs gen-except Core Foundations Codata Experiments
Everythings.hs: ./Cubical/Data/DescendingList/Strict.agda: hGetContents: invalid argument (invalid byte sequence)
make: *** [GNUmakefile:30: gen-everythings] Error 1
builder for '/nix/store/1xsk4ln5yi13y5s0cn1i57ccl42nchj9-cubical-0.2.drv' failed with exit code 2
error: build of '/nix/store/1xsk4ln5yi13y5s0cn1i57ccl42nchj9-cubical-0.2.drv' failed

[ryanorendorff]

I just got the same error. I'll push up what I have at the moment.

[alexarice]

The problem doesn't happen outside a nix-build

[Saizan]

I believe the script expects the locale to be UTF-8, is that something that can be set for the build?

[alexarice]

I think it can

[Saizan]

One can test it with ghc -e "print System.IO.localeEncoding".

However make all is currently doing testing, it's not something useful for "installation"

[ryanorendorff]

The output from the localeEncoding is ASCII. I'll try to change it to UTF-8.

[alexarice]

I think LC_ALL = "en_US.UTF-8"; is what we are looking for with the locale

[ryanorendorff]

I think LC_ALL = "en_US.UTF-8"; is what we are looking for with the locale

Hmm this leads to fun other errors:

runhaskell ./Everythings.hs gen-except Core Foundations Codata Experiments
/nix/store/81wybawvkr95c7j8gj5ab3y740mq1fli-bash-4.4-p23/bin/sh: warning: setlocale: LC_ALL: cannot change locale (en_US.UTF-8)
/nix/store/81wybawvkr95c7j8gj5ab3y740mq1fli-bash-4.4-p23/bin/sh: warning: setlocale: LC_ALL: cannot change locale (en_US.UTF-8)
/nix/store/81wybawvkr95c7j8gj5ab3y740mq1fli-bash-4.4-p23/bin/bash: warning: setlocale: LC_ALL: cannot change locale (en_US.UTF-8)
/nix/store/81wybawvkr95c7j8gj5ab3y740mq1fli-bash-4.4-p23/bin/bash: warning: setlocale: LC_ALL: cannot change locale (en_US.UTF-8)
/nix/store/81wybawvkr95c7j8gj5ab3y740mq1fli-bash-4.4-p23/bin/bash: warning: setlocale: LC_ALL: cannot change locale (en_US.UTF-8)
/nix/store/81wybawvkr95c7j8gj5ab3y740mq1fli-bash-4.4-p23/bin/bash: warning: setlocale: LC_ALL: cannot change locale (en_US.UTF-8)
Everythings.hs: ./Cubical/Data/DescendingList/Strict.agda: hGetContents: invalid argument (invalid byte sequence)
make: *** [GNUmakefile:30: gen-everythings] Error 1
builder for '/nix/store/kh89hx2jpkz4kfy3rzwsdvvvpwdjhi37-cubical-0.2.drv' failed with exit code 2

[alexarice]

Try to add glibcLocales to buildInputs? EDIT: Probably nativeBuildInputs

[ryanorendorff]

Try to add glibcLocales to buildInputs? EDIT: Probably nativeBuildInputs

Yes that worked. Building now.

[ryanorendorff]

Builds correctly and I was able to type check some cubical code that I had.

[alexarice]

Nix-review passes
Package builds on nixos
Looks ready apart from rebase

[alexarice]

@GrahamcOfBorg build agdaPackages.cubical

[laMudri]

Does this not affect nearly every other Agda package? It feels like it should be the default.

[alexarice]

Maybe though we haven't run into this problem before. Also this only seems to arise on the haskell building of Everything files and I don't think it is to do with agda I'm not sure it is correct to add it to the builder

[laMudri]

Aah, okay, that explains a bit what's going on. I see stdlib's equivalent Haskell file makes sure everything is done in UTF-8, which is probably the right thing to do upstream.

[alexarice]

Thanks @ryanorendorff , @Saizan , and @veprbl for merging 😄