Stream: Coq Workshop 2021

Topic: [S1T3] A Nix toolbox for reproducible Coq environments ...


view this post on Zulip Christian Doczkal (Jul 02 2021 at 08:55):

Presentation given by @Cyril Cohen

view this post on Zulip Andrej Dudenhefner (Jul 02 2021 at 09:11):

What are the pros and cons compared to opam dependency management?

view this post on Zulip Michael Soegtrop (Jul 02 2021 at 09:17):

I would say the caching is a nice feature for the CO2 footprint of Coq.

view this post on Zulip Yves Bertot (Jul 02 2021 at 09:19):

I really like the stance on reproducibility, too!

view this post on Zulip Cyril Cohen (Jul 02 2021 at 09:20):

Andrej Dudenhefner said:

What are the pros and cons compared to opam dependency management?

Another advantage is that the rev dep testing is a one-liner

view this post on Zulip Ben Siraphob (Jul 02 2021 at 09:20):

Are there plans to add compatibility with Nix flakes?

view this post on Zulip 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

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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:

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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: Aug 11 2022 at 01:03 UTC