Christian Doczkal (Jul 02 2021 at 08:55): Christian Doczkal (Jul 02 2021 at 08:55):Presentation given by @Cyril Cohen
Andrej Dudenhefner (Jul 02 2021 at 09:11):What are the pros and cons compared to opam dependency management?
Michael Soegtrop (Jul 02 2021 at 09:17):I would say the caching is a nice feature for the CO2 footprint of Coq.
Yves Bertot (Jul 02 2021 at 09:19):I really like the stance on reproducibility, too!
Cyril Cohen (Jul 02 2021 at 09:20):Andrej Dudenhefner said:
What are the pros and cons compared to
opamdependency management?
Another advantage is that the rev dep testing is a one-liner
Ben Siraphob (Jul 02 2021 at 09:20):Are there plans to add compatibility with Nix flakes?
Cyril Cohen (Jul 02 2021 at 09:20):Ben Siraphob said:
Are there plans to add compatibility with Nix flakes?
No plan, yet, I am still waiting for a doc to be available somewhere
Christian Doczkal (Jul 02 2021 at 09:24):Michael Soegtrop said:
I would say the caching is a nice feature for the CO2 footprint of Coq.
Yes, and that in addition to drastically cut down on CI runtimes for projects depending on heavy reverse dependencies of mathcomp such as coq-fourcolor. I really should migrate coq-graph-theory. :smile:
Théo Zimmermann (Jul 02 2021 at 09:27):In the Coq Nix Toolbox repository, we test the whole Coq package set from nixpkgs. Sometimes (if there were not many changes from the previous test) we can see the whole thing complete in minutes because of caching.
Christian Doczkal (Jul 02 2021 at 09:27):Well, for now CI is broken as I am using non-forgetful inheritance and the development version of HB still turns this into an error that I cannot circumvent without breaking things for the stable release :neutral:
Cyril Cohen (Jul 02 2021 at 09:30):Christian Doczkal said:
Well, for now CI is broken as I am using non-forgetful inheritance and the development version of HB still turns this into an error that I cannot circumvent without breaking things for the stable release :neutral:
you can instruct your .nix/config.nix to pick a version of HB just before the NFI test.
Théo Zimmermann (Jul 02 2021 at 09:34):Indeed, one thing that we didn't demo is that it's very easy to depend on a non-released version, be it a branch, a PR, etc. See also the examples for getting custom versions of Coq at https://github.com/coq/coq/wiki/Nix#coq-nix-toolbox
Enrico Tassi (Jul 02 2021 at 09:50):@Christian Doczkal it's fixed in this PR, yet to be merged: https://github.com/math-comp/hierarchy-builder/pull/252
Andrej Dudenhefner (Jul 02 2021 at 13:08):I tried out nix-shell https://coq.inria.fr/nix/toolbox --arg override '{coq = "master";}' under Windows 10 in wsl2 combined with vscode and it seems to work fine.
Last updated: Oct 04 2023 at 23:01 UTC