Advices on how to propagate ocaml's stdlib-shims · Nix toolbox devs & users

I had to add ocaml's package stdlib-shims to the derivation of metacoq some time ago (modification inspired from mathcomp I think) and it looks like it build fine upstream (eg. in nixpkgs the CI is green with the modified derivation) however just upating metacoq's CI to use a recent enough master does not work, stdlib-shims is not added as a dependency (see here). I found a way around that works locally on my machine and also on themetacoq CI (see here) but I don't understand how reasonable that script is.

Any recomendations on how to add this stdlib-shims ? I guess multiple coq packages defining plugins will have to use it for 8.16...

Théo Zimmermann (Sep 19 2022 at 10:52):

I don't quite understand what would explain why the dependency is used in one case and not in the other.

Théo Zimmermann (Sep 19 2022 at 10:54):

And the line you point to where you test on defaultVersion looks fishy anyway.

Kenji Maillard (Sep 19 2022 at 11:48):

yes, I tried testing on version and got an error on the comparison function (I guess that version variable is either undefined or not what I expect)

Théo Zimmermann (Sep 19 2022 at 12:04):

To be able to test on version you need to do something like what you did in nixpkgs, i.e., do it after the derivation has computed the version value.

Kenji Maillard (Sep 19 2022 at 12:08):

Any idea why the thing I did on nixpkgs does not work on metacoq's CI and locally on my machine though ?

Théo Zimmermann (Sep 19 2022 at 12:31):

Théo Zimmermann (Sep 19 2022 at 14:11):

Théo Zimmermann (Sep 19 2022 at 14:14):

Théo Zimmermann (Sep 19 2022 at 14:15):

diff --git a/.nix/coq-overlays/metacoq/default.nix b/.nix/coq-overlays/metacoq/default.nix
index 268ce247..a7985f23 100644
--- a/.nix/coq-overlays/metacoq/default.nix
+++ b/.nix/coq-overlays/metacoq/default.nix
@@ -77,7 +77,7 @@ let
         { passthru = genAttrs packages metacoq_; })
       ).overrideAttrs (o: {
         propagatedBuildInputs = o.propagatedBuildInputs ++
-          optional (versionAtLeast o.version "1.0-8.16") coq.ocamlPackages.stdlib-shims;
+          optional (versionAtLeast o.version "1.0-8.16" || o.version == "dev") coq.ocamlPackages.stdlib-shims;
       });
     in derivation;
 in

Théo Zimmermann (Sep 19 2022 at 14:16):

Unfortunately the "dev" value is not ordered as we would like so when we check that we are beyond a certain version, we have to also consider the dev case.

Kenji Maillard (Sep 19 2022 at 14:28):

hm, this create a small discrepancy on our older branches that did not seem to need stdlib-shims (the coq-8.14 and coq-8.15 branches). I guess it is still better than my previous hack...

Matthieu Sozeau (Sep 19 2022 at 14:35):

Kenji Maillard (Sep 19 2022 at 14:39):

Just tried a variation on your proposition @Théo Zimmermann (here, if it works fine for the CI I'll submit a PR to the nixpkgs

Stream: Nix toolbox devs & users

Topic: Advices on how to propagate ocaml's stdlib-shims

Kenji Maillard (Sep 19 2022 at 09:37):