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,
We must preserve:
config.nix
bundle configurations, it is ok if it requires light editions of a file. I am undecided whether this should be in the flake.nix
or not.Additionally we must use flakes locking instead of the commands updateNixToolBox
, updateNixpkgs
, updateNixpkgsMaster
etc.
The following commands can be turned into flakes app instead of shellHook: ppBundles
, ppBundleSet
, fetchCoqOverlay
, createOverlay
, cachedMake
, genNixActions
.
The following should be handled by nix flake init
instead generateNixDefault
, initNixConfig
.
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.
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:
genNixActions
generates the "initial" configurations from the defaultVersion
-switch in the default.nix
files in nixpkgs
.config.nix
, are loaded when the CI is running and this may in fact turn a schedule configuration into a noop.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.
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).
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?
Sebastian Ertel said:
I thought that
genNixActions
is based only onnixpkgs
. But the bundles are defined in thedefault.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.
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:
Thanks for you help!
Sorry I do not have much time but here is the entry point :up:
I will come back later this weekend or on Monday.
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.
FTR I originally intended to build upon the current nix toolbox to get a flakes setup, is that what you are doing @Sebastian Ertel ?
@Cyril Cohen , yes, that is exactly what I'm trying to do. Although there are two steps for me
mkCoqDerivation
etc.) available on nixpkgs to build coq-modules as flakes and load them as dependencies into application projects as a flake input.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.
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!
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?
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.
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.
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 bymkDerivation
and variants make sure to run the env hooks that were declared that way. So thisaddCoqPath
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.
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.
Following what you wrote, I now need to enlist ssprove
as a reverse dependency for coq
.
I tried to do so "manually" but that did not work.
Sebastian Ertel said:
Following what you wrote, I now need to enlist
ssprove
as a reverse dependency forcoq
.
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.
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.
It exports also mkDrv
which is a wrapper around mkCoqDerivation
.
That way I can let the calling script chose which version of Coq and its packages are loaded.
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?
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.
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.
But this is the way the other modules work as well.
They all depend on a Coq version as their package input.
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.
It seems wrong or at least strange to me to have a default version here.
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.
But I can certainly give this a try as well later this evening.
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.)
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
.
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:
Some details:
flake.lock
. 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.flake.nix
and flake.lock
to a repository.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).
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:
flake.lock
files.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:
coq-8.16
and mathcomp-2.0.0
.Similarly,
coq-8.18
and mathcomp-2.2.0
.coq-8.18
and mathcomp-2.1.0
(which is not checked via the CI).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?
We designed the nix CI with the following features in mind:
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)
For me the flakes migration should only subsume the components of the toolbox that can be taken in charge by flakes, i.e.:
Thanks @Cyril Cohen for this explanation.
That makes sense to me.
I think I would phrase some goals for supporting flakes like so:
nixpkgs
repo.I'm still not sure how to move forward on this side.
I could envision the following:
coq-nix-toolbox
becomes a flake itself.coq-nix-toolbox
becomes a passthrough for coq packages. coq-nix-toolbox
.Questions that I did not resolve yet:
coq-nix-toolbox
with an according PR and a passing CI (instead of new version of nixpkgs
).follows
to the according version in the coq-nix-toolbox
.)coq-nix-toolbox
, would it make sense to load them directly from the library repositories?This whole setup should make it very easy for even non-nix developers to make their project available.
coq-nix-toolbox
.Does that make sense to you or did you envision something entirely different?
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:
- The coq-nix-toolbox becomes a flake itself.
:check:
- CoqPackages loaded via this flake are guaranteed to be working.
:check:
- That is, coq-nix-toolbox becomes a passthrough for coq packages.
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.
- Developers that want to make sure to get a working version load via the coq package via the coq-nix-toolbox.
Do you mean developers that want a specific set of dependencies and reverse dependencies load them via the coq-nix-toolbox?
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.nix
file 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.
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)
- Define your own CI job locally.
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...
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).
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).
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.
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.
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.
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
.
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.
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.
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