Stream: Nix toolbox devs & users

Topic: Ssreflect via Nix toolbox

view this post on Zulip Arthur Azevedo de Amorim (May 16 2023 at 15:37):

I am trying to set up an environment with ssreflect 2.0.0. Here are the relevant lines of my config.nix file:

buildInputs = [ "mathcomp-ssreflect" ];

/* ... */

bundles.default = {
  coqPackages.coq.override.version = "8.17";
  coqPackages.mathcomp.ssreflect.override.version = "2.0.0";
};

If I run nix-shell, however, it is version 1.16 that is pulled up, not 2.0.0.

I have also tried pulling in all of mathcomp 2.0.0, by using "mathcomp" as a build input, and by using coqPackages.mathcomp.override.version = "2.0.0"; in the above snippet. This works, but I would rather avoid the unnecessary dependencies...

view this post on Zulip Pierre Roux (May 16 2023 at 15:50):

Maybe you can coqPackages.mathcomp.fingroup.job = false, coqPackages.mathcomp.algebra.job = false and so on (not great though)

view this post on Zulip Arthur Azevedo de Amorim (May 16 2023 at 15:51):

@Pierre Roux Do you mean writing coqPackages.mathcomp.fingroup.override.job = false;
?

view this post on Zulip Pierre Roux (May 16 2023 at 15:53):

without the override yes

view this post on Zulip Arthur Azevedo de Amorim (May 16 2023 at 16:05):

@Pierre Roux Is there any way of testing whether this works without garbage collecting the previous derivations? I just ran nix-shell --pure with the modified file, but it seems that it is just finding the packages that I had built earlier.

view this post on Zulip Pierre Roux (May 16 2023 at 16:17):

Maybe modifying the code to force recompilation? I don't know.

view this post on Zulip Théo Zimmermann (May 16 2023 at 21:59):

First, mathcomp is a bit peculiar. You need to override the version of coqPackages.mathcomp even if what you are putting in your buildInputs is mathcomp-ssreflect and nothing more.

view this post on Zulip Théo Zimmermann (May 16 2023 at 22:00):

Second, there is no need to garbage collect anything. If it is still finding the packages that you had built earlier, then somehow it means that you have not changed what it evaluates. Nix is functional in the sense that packages are pure functions of their inputs. So no side effect, like garbage-collection, should have any impact on the result.

view this post on Zulip Arthur Azevedo de Amorim (May 30 2023 at 06:56):

@Théo Zimmermann That worked! Thanks.

Last updated: Nov 29 2023 at 21:01 UTC