Stream: Nix toolbox devs & users

Topic: Switch to flakes brainstorming


view this post on Zulip Cyril Cohen (Feb 01 2024 at 11:52):

Hi @Sebastian Ertel @Théo Zimmermann.
Here are my thoughts on the switch to flakes.

The switch to flakes must preserve the two main functionalities of the toolbox: reproducible development environement and CI with reverse dependencies and caching.

In details,

view this post on Zulip Sebastian Ertel (Feb 01 2024 at 16:16):

Hi @Cyril Cohen ,
thanks for sharing your thoughts. I still have to understand first what all these functions do before I can evaluate the effort that is behind this switch to flakes.
In order to do so, I will try to build a flake for one repo while preserving most of the machinery that already exists which understandably was one of your main requirements.

view this post on Zulip Sebastian Ertel (Feb 11 2024 at 12:29):

So now that I have at least some idea on how the coq-nix-toolbox works, I have the following questions:

Apart from replacing certain parts of the current toolbox with flake functionality, what benefit do you intent to achieve with this switch to flakes?

For example, the CI is tightly coupled to PRs against the nixpkgs repo. Do you intent to bring this process all into the coq-nix-toolbox to remove the nixpkgs PRs from the whole workflow?
To me, this seems to makes sense because then everything would be in the same repo. That is, the coq-nix-toolbox would itself become a flake and loading packages in a project's flake would then be coq-nix-toolbox.coqPackages instead of nixpkgs.legacyPackages.${system}.coqPackages.

Another example is the configuration of the bundles to be executed by the CI for a coq module.
Currently, as far as I have understood this, there are 2 parts of the CI that figure out what the final configuration (mostly coq and mathcomp) is:

  1. genNixActions generates the "initial" configurations from the defaultVersion-switch in the default.nix files in nixpkgs.
  2. Release-specific configurations, i.e., the bundles in the project-local config.nix, are loaded when the CI is running and this may in fact turn a schedule configuration into a noop.
    That is, the information in 1 (often) includes the information from 2.
    Do you wish to consolidate these two steps somehow?

view this post on Zulip Théo Zimmermann (Feb 13 2024 at 11:47):

For example, the CI is tightly coupled to PRs against the nixpkgs repo. Do you intent to bring this process all into the coq-nix-toolbox to remove the nixpkgs PRs from the whole workflow?

No, IMHO at least to start with, we would keep the Coq packages within nixpkgs.

view this post on Zulip Théo Zimmermann (Feb 13 2024 at 11:49):

I'm not sure what you mean about CI, but genNixActions currently generates as many workflows as there are bundles. There is nothing dynamic in the CI configuration currently (we might want to have some dynamic configuration to speed things up when there is not much to rebuild, but that's a separate discussion).

view this post on Zulip Sebastian Ertel (Feb 13 2024 at 11:57):

I thought that genNixActions is based only on nixpkgs. But the bundles are defined in the default.nix files of the individual module repos. This makes sense because bundles are defined on a release basis.

Hence, genNixActions only uses the version switch statement. But that could allow for more configurations than bundles being defined.

That is how I thought the CI of coq-nix-toolbox works and this is the CI that we are talking about here, right?

view this post on Zulip Théo Zimmermann (Feb 22 2024 at 14:46):

Sebastian Ertel said:

I thought that genNixActions is based only on nixpkgs. But the bundles are defined in the default.nix files of the individual module repos. This makes sense because bundles are defined on a release basis.

Hence, genNixActions only uses the version switch statement. But that could allow for more configurations than bundles being defined.

That is how I thought the CI of coq-nix-toolbox works and this is the CI that we are talking about here, right?

Sorry for the long delay. I think we are talking about CI that can be generated using the Coq Nix Toolbox in general, for any project, including the toolbox itself. Usually, the bundles are defined in .nix/config.nix but for the Coq Nix Toolbox, they are defined in .nix/fallback-config.nix for some reason that I don't remember very clearly about: https://github.com/coq-community/coq-nix-toolbox/blob/a1ebdd160bc8abbc4b3efbb654235fa0206e1fb9/.nix/fallback-config.nix#L21
We have to update this line to test new releases.

view this post on Zulip Sebastian Ertel (Mar 15 2024 at 15:56):

Hi @Cyril Cohen and @Théo Zimmermann ,

I'm currently working on a first flakes-based setup and I face the problem that I cannot quite figure out how Coq libraries get loaded onto the COQPATH. I saw that this happens in the setupHook of the Coq derivation.
But I cannot understand how the Nix/Shell code understands which libraries get added to the COQPATH.
So my questions are:

  1. How do libraries end up on the COQPATH?
  2. How can I add a Coq library that is not located in nixpkgs but is loaded as a flake input to the COQPATH?

Thanks for you help!

view this post on Zulip Cyril Cohen (Mar 15 2024 at 16:24):

https://github.com/sertel/nixpkgs/blob/4ccd0ac4aec0f5750ebd6af7b251eb0fbb1319ec/pkgs/applications/science/logic/coq/default.nix#L168-L173

view this post on Zulip Cyril Cohen (Mar 15 2024 at 16:25):

Sorry I do not have much time but here is the entry point :up:
I will come back later this weekend or on Monday.

view this post on Zulip Théo Zimmermann (Mar 15 2024 at 16:31):

The principle of the setup hook (https://nixos.org/manual/nixpkgs/stable/#ssec-setup-hooks) is that it is run by all the packages that depend on Coq. So basically, packages add themselves to COQPATH. I don't think that not being in nixpkgs should make any difference here. But I admit I have never looked very deeply at how setup hooks work.

view this post on Zulip Cyril Cohen (Mar 15 2024 at 16:31):

FTR I originally intended to build upon the current nix toolbox to get a flakes setup, is that what you are doing @Sebastian Ertel ?

view this post on Zulip Sebastian Ertel (Mar 15 2024 at 19:36):

@Cyril Cohen , yes, that is exactly what I'm trying to do. Although there are two steps for me

  1. Use the coq-nix "framework" (mkCoqDerivation etc.) available on nixpkgs to build coq-modules as flakes and load them as dependencies into application projects as a flake input.
  2. Take a look at the coq-nix-toolbox to see what I need to add in order to allow the libraries that are flakes and therefore not in nixpkgs to nevertheless be part of the CI (which is a Github action in coq-nix-toolbox).

I thought that was also in line with what you had in mind. Please correct me if I'm mistaken.

view this post on Zulip Sebastian Ertel (Mar 15 2024 at 19:37):

Cyril Cohen schrieb:

Sorry I do not have much time but here is the entry point :up:
I will come back later this weekend or on Monday.

There is no need to reply on the weekend. Monday is totally fine for me!

view this post on Zulip Sebastian Ertel (Mar 15 2024 at 19:41):

Thanks for the entry point and the explanation for the setupHook.
Indeed I found all these.

However, the part that I do not understand is this:
Only the Coq derivation runs the setupHook, none of the coq-modules does.
At least this is what I see when I investigate the derivations via:
nix derivation show nixpkgs#coqPackages_8_18.extructures (as an example)
and
nix derivation show nixpkgs#coq_8_18
So how come each of the modules ends up in the COQPATH when they do not run the setupHook?
Or am I misreading the derivations?

view this post on Zulip Théo Zimmermann (Mar 18 2024 at 12:56):

The setup hook declares a bash function, then runs addEnvHooks (https://github.com/sertel/nixpkgs/blob/4ccd0ac4aec0f5750ebd6af7b251eb0fbb1319ec/pkgs/applications/science/logic/coq/default.nix#L175). The standard env setup used by mkDerivation and variants make sure to run the env hooks that were declared that way. So this addCoqPath function is run by all reverse dependencies of the Coq derivation, as opposed to Coq itself.

view this post on Zulip Théo Zimmermann (Mar 18 2024 at 12:58):

Did you test defining Coq packages inside flakes yet? Maybe you should start working on an example and let us know if you encounter any difficulties.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 13:13):

Théo Zimmermann schrieb:

The setup hook declares a bash function, then runs addEnvHooks (https://github.com/sertel/nixpkgs/blob/4ccd0ac4aec0f5750ebd6af7b251eb0fbb1319ec/pkgs/applications/science/logic/coq/default.nix#L175). The standard env setup used by mkDerivation and variants make sure to run the env hooks that were declared that way. So this addCoqPath function is run by all reverse dependencies of the Coq derivation, as opposed to Coq itself.

I see. Thanks for the explanation. That makes perfect sense now.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 13:32):

Théo Zimmermann schrieb:

Did you test defining Coq packages inside flakes yet? Maybe you should start working on an example and let us know if you encounter any difficulties.

I'm happy to share it.
I'm using SSProve as a running example of a library and our application using SSProve.
Here is the flake of the SSProve library.
I'm loading SSProve as a flake input in this flake.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 13:34):

Following what you wrote, I now need to enlist ssprove as a reverse dependency for coq.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 13:36):

I tried to do so "manually" but that did not work.

view this post on Zulip Théo Zimmermann (Mar 18 2024 at 16:24):

Sebastian Ertel said:

Following what you wrote, I now need to enlist ssprove as a reverse dependency for coq.

I don't understand this. If you are able to build ssprove, then it has Coq as a dependency, and thus it is a reverse dependency for Coq. You have nothing to declare / enlist.

view this post on Zulip Théo Zimmermann (Mar 18 2024 at 16:27):

In the code of your flake for SSProve, something seems strange to me. It only exports a devShell, no package, so I don't get how you can hope to reuse it from another flake.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:52):

It exports also mkDrv which is a wrapper around mkCoqDerivation.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:53):

That way I can let the calling script chose which version of Coq and its packages are loaded.

view this post on Zulip Théo Zimmermann (Mar 18 2024 at 16:54):

Do you know about the override mechanism used in nixpkgs? Wouldn't it be better to export a package and use this mechanism for changing the versions?

view this post on Zulip Cyril Cohen (Mar 18 2024 at 16:54):

Sebastian Ertel said:

That way I can let the calling script chose which version of Coq and its packages are loaded.

The way this is done in nixpkgs is by overriding an existing derivation: you start from a potentially broken one and call override to change potentially any input derivation.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:54):

After reading up on the environment hooks, my feeling is that for some reason the Coq derivation does not make it into the propagatedBuildInputs of the SSProve derivation.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:56):

But this is the way the other modules work as well.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:56):

They all depend on a Coq version as their package input.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:57):

The only difference is that these versions are all prebuilt for all the individual Coq versions available in nixpkgs. Other than that I cannot see a difference.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:58):

It seems wrong or at least strange to me to have a default version here.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 16:59):

Indeed I so far left out the version switch statement that dispatches the different releases of the module depending on the Coq and potentially math comp versions.

view this post on Zulip Sebastian Ertel (Mar 18 2024 at 17:03):

But I can certainly give this a try as well later this evening.

view this post on Zulip Sebastian Ertel (Mar 20 2024 at 15:50):

I found the problem: src = "./."; vs. src = ./.; :man_facepalming:
(It would have been great if Nix would have actually reported an error on this one instead of doing just nothing.)

view this post on Zulip Sebastian Ertel (Mar 20 2024 at 15:54):

This "completes" my first goal.
The switch statement in the SSProve derivation is still missing but that is mainly because there is no versioning yet in SSProve. I will also try to load mathcomp-extra this way where versioning is available.
Afterwards, I will check on what I need to do in order to run flake-based coq modules in the CI of coq-nix-toolbox.

view this post on Zulip Sebastian Ertel (Mar 28 2024 at 20:47):

So, I played a little bit with the version switch just to arrive at the following conclusion (that the two of you were probably fully aware of): when switching to flakes such a switch statement does not make sense anymore. In fact, it would not even work.

You can again have a look at my try:

view this post on Zulip Sebastian Ertel (Mar 28 2024 at 20:56):

Some details:

  1. Notice the switch is now backwards, i.e., from the library to its dependencies. The coq-modules in nixpkgs do this the other way around. They say: "For a given coq or mathcomp version, you have to use this release." The switch in the flake needs to find the versions of the dependencies (coq and mathcomp) using the revision of the library loaded via the flake. This makes sense because versioning is controlled via flake.lock.
  2. Because of that even the entire switch statement does not make sense anymore. Versioning is entirely via the flake.lock. That means, the flake.lock of mathcomp-extra has all the dependencies and their versions for the current revision of mathcomp-extra. If an update occurs then the flake.lock is also updated. To get the old configuration, all I need to do is load the old revision from the repository.
  3. That automatically has the following implication: it is not possible to support older versions of libraries via flakes. This support needs to still be provided via nixpkgs. Flake support and the associated versions that can be loaded via the flake start at the commit that adds the flake.nix and flake.lock to a repository.

view this post on Zulip Sebastian Ertel (Mar 28 2024 at 21:03):

For supporting flakes in the CI, this means that the bundles are essentially not necessary anymore. All that is needed is a list of versions with flake support (,i.e., with flake.nix and flake.lock files).

view this post on Zulip Sebastian Ertel (Apr 02 2024 at 09:53):

I have been thinking about this for a while and I'm at the point where I need to understand the following question:
What is the purpose of the CI?
Phased a little bit differently:
What do libraries and their respective authors expect when they are on the CI?

I'm asking this for the following reasons:

Currently, the setup allows to load a version of a library that is broken. This is possible because not all version permutations are tested in the CI.
Here is mathcomp-analysis as an example:

Similarly,

That is, it seems to me that the developer cannot rely on the fact that everything that can be loaded via the version switch in nixpkgs is actually working properly.

With flakes, one goal can be that there is at least one CI revision for every version of a library. That makes sure that every library with a respective set of dependencies, was working. But then the question remains: Why would that not be possible in the library repos themselves?

view this post on Zulip Cyril Cohen (Apr 02 2024 at 12:44):

We designed the nix CI with the following features in mind:

  1. test that the nixpkgs version switches are all ok (this is obviously wrongly implemented since you found non compiling code)
  2. for each package in the Coq ecosystem on nix (e.g. math-comp), be able to test whether the master version of a given package compiles with the expected versions of Coq and with either released, master or specific branches of reverse dependencies (e.g. mathcomp analysis)
  3. produce binaries so that one can instatenously reproduce a working PR or any othe environements of a breaking PR.

view this post on Zulip Cyril Cohen (Apr 02 2024 at 12:48):

The toolbox does not only provide the CI, although it was a goal that the same environements as for developers should be used by the CI, hence the reuse of the bundles declared by the toolbox.
Indeed, it is supposed to provide an easy way to override various packages, or add new ones, without going through heavy manipulations of nixpkgs (e.g. forking or manual overriding though explicit calls to overrideScope), so that people with no knowledge of nix can add / change a new override from the configuration file, by reading it as a purely declarative static record (like json)

view this post on Zulip Cyril Cohen (Apr 02 2024 at 13:19):

For me the flakes migration should only subsume the components of the toolbox that can be taken in charge by flakes, i.e.:

view this post on Zulip Sebastian Ertel (Apr 02 2024 at 14:15):

Thanks @Cyril Cohen for this explanation.
That makes sense to me.

I think I would phrase some goals for supporting flakes like so:

I'm still not sure how to move forward on this side.

I could envision the following:

Questions that I did not resolve yet:

This whole setup should make it very easy for even non-nix developers to make their project available.

  1. Write a flake from a template that is provided.
  2. Define your own CI job locally.
  3. Register your library via a PR at the coq-nix-toolbox.

Does that make sense to you or did you envision something entirely different?

view this post on Zulip Cyril Cohen (Apr 03 2024 at 11:28):

Hi @Sebastian Ertel,

For libraries based on flakes there should be no two version switches (nixpkgs vs. bundles).

I do not understand what you mean by "libraries based on flakes". My intention was that every library handled by the toolbox adds itself to nixpkgs in one way (directly in the repo) or another (as an overlay). A currently missing feature would be the transitivity of overlays. I'd like to discuss that topic at some point because it would lead to a nontrivial cleanup of the current infrastructure.

I could envision the following:
- The current CI and nixpkgs stays unchanged.

:check:

:check:

:check:

I'm not sure I understand what you mean by "becomes a passthrough", the coq-nix-toolbox would rather be an augmented overlay for coq (and ocaml) packages.

Do you mean developers that want a specific set of dependencies and reverse dependencies load them via the coq-nix-toolbox?

view this post on Zulip Cyril Cohen (Apr 03 2024 at 11:39):

Questions that I did not resolve yet:
- Every version update of a library now becomes an update of the coq-nix-toolbox with an according PR and a passing CI (instead of new version of nixpkgs).

Currently subsequent master revisions of the coq-nix-toolbox only pin a new master nixpkgs. (Other branches are only made for testing PR to nixpkgs itself, and thus anticipating incompatible package sets). In think that it would be good to preserve this model, but implement it via flakes locks instead.

How does one easily find the correct revisions? For example, I would like to load version XYZ for mathcomp-analysis via coq-nix-toolbox. (I wonder if it is possible to load the version from the library repo and then link it with follows to the according version in the coq-nix-toolbox.)

Currently it is done through the .nix/config.nixfile in the repo of the package where one wants to update to this or that version. It could either stay there with an additional feature to refer to attribues in the flakes input (so that we can take advantage of the locking feature and preserve backward compatibility of the old config files), or be moved entirely to the flakes.nix file, I'm open to many solutions.

Instead of defining the CI jobs in coq-nix-toolbox, would it make sense to load them directly from the library repositories?

They are already generated on a repository basis. The one in the coq-nix-toolbox tests everything, while local CIs test only their own deps, themselves and their own reverse dependencies. This maximal sharing of infrastructure and caching ensures that untouched reverse dependencies are actually compiled once and exactly once (in the coq-nix-toolbox) and stored in cache.

view this post on Zulip Cyril Cohen (Apr 03 2024 at 11:49):

This whole setup should make it very easy for even non-nix developers to make their project available.
- Write a flake from a template that is provided.

Ideally no one has to write a flakes, but use the init command. They can then slightly edit the file but it's already not a template anymore. This would hopefully replace the steps:

nix-env -iA nixpkgs.cachix && cachix use coq && cachix use coq-community && cachix use math-comp
nix-shell https://github.com/coq-community/coq-nix-toolbox/archive/master.tar.gz --arg do-nothing true --run generateNixDefault
nix-shell --arg do-nothing true --run "initNixConfig YOURPACKAGENAME"

from the current https://github.com/coq-community/coq-nix-toolbox
and leave you to edit .nix/config.nix as before (or its replacement should it ever happen)

Ideally there would be an app (see the apps line in the doc) for that, e.g.

nix run .#genCI

replacing the ugly

nix-shell --arg do-nothing true --run "genNixActions"

Register your library via a PR at the coq-nix-toolbox.

Ideally library are registered first and foremost to nixpkgs, and there could be an app

nix run .#submitDerivationPR <name>

But with a proper cascading of overlay starting from nixpkgs and passing through coq-nix-toolbox, and various dependencies before reaching the final overlays in the current repo, it could be appropriate to submit the PR to various places. I'm not sure...

view this post on Zulip Sebastian Ertel (Apr 03 2024 at 12:19):

Hi @Cyril Cohen ,
Thanks for the explanations.
I'm still struggling with the point that everything should be inside nixpkgs. Flakes are supposed to resolve this mono-repo design. That is why I do not understand why everything should still be in nixpkgs rather than in coq-nix-toolbox (or any other repo).

view this post on Zulip Sebastian Ertel (Apr 03 2024 at 12:27):

Cyril Cohen schrieb:

Do you mean developers that want a specific set of dependencies and reverse dependencies load them via the coq-nix-toolbox?

Yes, exactly.
When I now write nixpkgs.coqPackages.mathcomp-analysis then I would instead write coq-nix-toolbox.coqPackages.mathcomp-analysis (or something similar).

view this post on Zulip Sebastian Ertel (Apr 03 2024 at 12:30):

Cyril Cohen schrieb:

I'm not sure I understand what you mean by "becomes a passthrough", the coq-nix-toolbox would rather be an augmented overlay for coq (and ocaml) packages.

The coq-nix-toolbox essentially does not add anything new. It just provides a set of coqPackages from its flake inputs. The inputs of the coq-nix-toolbox are essentially all coq libraries/modules that contain a flake.

view this post on Zulip Sebastian Ertel (Apr 03 2024 at 12:32):

Cyril Cohen schrieb:

Currently subsequent master revisions of the coq-nix-toolbox only pin a new master nixpkgs. (Other branches are only made for testing PR to nixpkgs itself, and thus anticipating incompatible package sets). In think that it would be good to preserve this model, but implement it via flakes locks instead.

I have trouble to understand how this would be implemented via flakes locks.

view this post on Zulip Cyril Cohen (Apr 03 2024 at 12:33):

Sebastian Ertel said:

Hi Cyril Cohen ,
Thanks for the explanations.
I'm still struggling with the point that everything should be inside nixpkgs. Flakes are supposed to resolve this mono-repo design. That is why I do not understand why everything should still be in nixpkgs rather than in coq-nix-toolbox (or any other repo).

I'm not (yet) convinced by the obsolesence of the mono-repo approach. In particular I do not yet understand how to guarantee the existence of meaningful maximal set of packages. Furthermore nixpkgs is still wildly used and flakes is still at an early adoption stage, so I think it is a sound approach to fully support nixpkgs and not require that all packages migrated to flakes.

view this post on Zulip Sebastian Ertel (Apr 03 2024 at 12:36):

Cyril Cohen schrieb:

This whole setup should make it very easy for even non-nix developers to make their project available.
- Write a flake from a template that is provided.

Ideally no one has to write a flakes, but use the init command. They can then slightly edit the file but it's already not a template anymore. This would hopefully replace the steps:

nix-env -iA nixpkgs.cachix && cachix use coq && cachix use coq-community && cachix use math-comp
nix-shell https://github.com/coq-community/coq-nix-toolbox/archive/master.tar.gz --arg do-nothing true --run generateNixDefault
nix-shell --arg do-nothing true --run "initNixConfig YOURPACKAGENAME"

from the current https://github.com/coq-community/coq-nix-toolbox
and leave you to edit .nix/config.nix as before (or its replacement should it ever happen)

If the developer edits the config.nix as they do now and that gets loaded into the flake to provide the derivation is also fine with me.
This is just about editing the flake or config.nix.

view this post on Zulip Sebastian Ertel (Apr 03 2024 at 12:38):

Cyril Cohen schrieb:

I'm not (yet) convinced by the obsolesence of the mono-repo approach. In particular I do not yet understand how to guarantee the existence of meaningful maximal set of packages. Furthermore nixpkgs is still wildly used and flakes is still at an early adoption stage, so I think it is a sound approach to fully support nixpkgs and not require that all packages migrated to flakes.

Fair enough, that is why I was advocating a hybrid approach supporting nixpkgs-based and flake-based coq-modules.

view this post on Zulip Sebastian Ertel (Apr 03 2024 at 12:39):

Cyril Cohen schrieb:

Ideally there would be an app (see the apps line in the doc) for that, e.g.

nix run .#genCI

replacing the ugly

nix-shell --arg do-nothing true --run "genNixActions"

Sure.

view this post on Zulip Sebastian Ertel (Apr 04 2024 at 07:58):

For the record, there is also library support from the nix community to turn flakes into github action matrices. (I have yet to try this out though.)


Last updated: Oct 13 2024 at 01:02 UTC