Add Nix flakes

[guilhermehas]

With this flake file, it becomes easier to import this library into other projects.
This is based on:
https://github.com/NixOS/nixpkgs/blob/master/pkgs/build-support/agda/default.nix
https://github.com/NixOS/nixpkgs/blob/master/pkgs/development/libraries/agda/cubical/default.nix

[mortberg]

@MatthiasHu Can you please take a look at this :-)

[MatthiasHu]

Disclaimer: I am not familiar with nix flakes. :-)

I successfully tested the flake by running:

nix --extra-experimental-features "nix-command flakes" shell github:guilhermehas/cubical/7039feccf434861d16921522ebdf1bd2c3de5306

@guilhermehas Could you perhaps provide a minimal working example of how to import the library in another project via the flake file?

[guilhermehas]

cat << EOF > test.agda                                                                                                                           
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
EOF

nix --extra-experimental-features "nix-command flakes" shell github:guilhermehas/cubical/52dfed7b703e6294b7acd11244cd838480839367#agdaWithCubical

agda -l cubical -i . test.agda

With these commands, I can use the cubical library of Agda.

Do you want to document it in some file such as README.md? And try to make everything in just one command?

[mortberg]

cat << EOF > test.agda                                                                                                                           
{-# OPTIONS --cubical #-}
open import Cubical.Foundations.Prelude
EOF

nix --extra-experimental-features "nix-command flakes" shell github:guilhermehas/cubical/52dfed7b703e6294b7acd11244cd838480839367#agdaWithCubical

agda -l cubical -i . test.agda

With these commands, I can use the cubical library of Agda.

Do you want to document it in some file such as README.md? And try to make everything in just one command?

Maybe this would fit better in INSTALL.md?

[MatthiasHu]

Thank you, @guilhermehas !

I agree that INSTALL.md would be a good place to put the usage example. Perhaps in a short section called "Nix flakes instructions"?

[MatthiasHu]

Also, a question about .github/workflows/ci-nix.yml: I assume that this CI job checks the whole library, as part of building the flake, which is already done by ci-ubuntu.yml. So does this mean that the library will be checked twice on every push to a pull request? Or perhaps only on every push to the master branch? I am not sure what the line on: [push] means.

[guilhermehas]

I have put the instructions in INSTALL.md and also changed the CI to just work when deploying on the master branch.

[MatthiasHu]

I assume that the purpose of the Nix CI job is to check whether the (automatically generated) flake.lock file (which determines in particular the precise Agda version) needs to be updated after some changes to the library. If I understand you right, @guilhermehas, you would like this job to run (at least) whenever a PR is merged into master.

Then this raises the question who is responsible for updating flake.lock when the Nix CI job fails.

[MatthiasHu]

The procedure in the new section in INSTALL.md works for me.

[guilhermehas]

after some changes to the library. If I understand you right, @guilhermehas, you would like this job to run (at least) whenever a PR is merged into master.

I think that we need just to update the lock file if the library is using a feature of a newer compiler.
But if there is any problem with nix flakes, I will come here to fix it.

[mortberg]

Is this ready to be merged now? @MatthiasHu

Is there be anything us developers will have to do in the future for example when releasing a new version of the library when there is a new version of Agda out? @guilhermehas

[guilhermehas]

I tried to use this Agda flake, but it didn't work here. It looks like it is broken.

I put inputs.nixpkgs.url = "nixpkgs/nixos-22.05" , so now nixpkgs is pinned in one version.

[ncfavier]

Right, vector-hashtables is broken in 22.05. I guess that's fine.

Maybe the most flexible option is to also provide an overlay, just like the agda flake does, so that people can use this with whichever nixpkgs and Agda they want.

[mortberg]

Is there be anything us developers will have to do in the future for example when releasing a new version of the library when there is a new version of Agda out?

You'll at least need to bump the version in flake.nix. The Agda version used here is tied to the version in nixpkgs, so you'll have to wait for it to land in nixpkgs and then do nix flake lock --update-input nixpkgs.

A probably better alternative would be to use the Agda flake so that we can pin Agda to whatever version we need.

Ok, I can already now promise that I will forget to do this... Is there some way of doing this that doesn't require any effort for us developers?

[ncfavier]

There is an action for automatically updating the lockfile and sending PRs: https://github.com/DeterminateSystems/update-flake-lock

[ncfavier]

Also, whatever steps need to be taken could just be documented in RELEASE.md :)

[mortberg]

Also, whatever steps need to be taken could just be documented in RELEASE.md :)

That would be great!

[guilhermehas]

@ncfavier I created an overlay. Look if it is good.
I don't know if it is possible to change the Agda compiler using my overlay.

[guilhermehas]

Also, whatever steps need to be taken could just be documented in RELEASE.md :)

I put the instructions in RELEASE.md.

[felixwellen]

@guilhermehas : What is the status of this PR? Does it need more testing?

[guilhermehas]

@guilhermehas : What is the status of this PR? Does it need more testing?

For me, it is done and it does not need more testing.

[phijor]

I've tested the Nix Flake, and it works as expected.

Apart from some minor issues, this looks ready to rebase, squash and merge.

[felixwellen]

@phijor : Thanks for joining!
@guilhermehas : Thanks for updating... Could you also rebase/merge master?

[guilhermehas]

@phijor : Thanks for joining! @guilhermehas : Thanks for updating... Could you also rebase/merge master?

I merged the master to it.

[felixwellen]

I assume the second, slow, apparently not cached ci job added by this PR is intended - I don't mind it since it doesn't seem to slow down the old ci job.

[felixwellen]

@guilhermehas : Feel free to use the "Resolve conversation" button in the conversations above, if you think something is resolved.

[guilhermehas]

@guilhermehas : Feel free to use the "Resolve conversation" button in the conversations above, if you think something is resolved.

I clicked to resolve the conversation.

[felixwellen]

Ok, then - looks like everything is resolved -> merging.