search

agda / cubical

An experimental library for Cubical Agda
https://agda.github.io/cubical/Cubical.README.html
Other
447 stars 136 forks source link

Added agda-2.6.3 in flakes #959

Closed guilhermehas closed 1 year ago

guilhermehas commented 1 year ago

Cubical Agda in Nix is compiled using Agda 2.6.3.

felixwellen commented 1 year ago

Nice! I don't understand why the old ci-ubuntu job doesn't run - do you know?

felixwellen commented 1 year ago

More questions:

guilhermehas commented 1 year ago

Nice! I don't understand why the old ci-ubuntu job doesn't run - do you know?

No, I don't know

For your example, the line will be:

inputs.agda.url = "github:agda/agda/?ref=v2.6.3";
  • How do nix flakes compose? If I have a project, that uses flake A and flake B, which both have agda defined as outputs, which agda will be available in the environment I get in the end?

It is composed using overlay: For example:

overlays = [ overlayAgda2 overlayAgda3 ];
pkgs = import nixpkgs { inherit overlays; };

Nixpkgs have Agda1, overlayAgda2 has Agda2 and overlayAgda3 has Agda3. I think that in the end, Agda3 will be used.

@MatthiasHu maybe can help if I explained anything wrong.

felixwellen commented 1 year ago

Thanks for explaining and for pointing me to the agda-version - I just overlooked that line in the diff...

MatthiasHu commented 1 year ago

Nice! I don't understand why the old ci-ubuntu job doesn't run - do you know?

That is because the ci-ubuntu workflow is configured to run on pull requests into master, but this is not a pull request into master. :-)

MatthiasHu commented 1 year ago

I was a bit confused why we have two versions of nixpkgs in flake.lock now, nixpkgs and nixpkgs_2 (and the same for flake-utils). I think this is because the Agda flake (in the version specified in our flake.lock) specifies (in its flake.lock) a different version of nixpkgs than our flake.lock does. I am not sure if this is the way it is supposed to be when you compose flakes, but I also don't see a good way to avoid it.

MatthiasHu commented 1 year ago

I think I understand now that we could declare that our nixpkgs input follows Agda's nixpkgs -- or the other way round. But it does not seem to be necessary: "[...] it is generally not useful to eliminate transitive nixpkgs flake inputs [...]". We could still do it for flake-utils, but probably it is not important.