Stream: Nix toolbox devs & users

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


view this post on Zulip Kenji Maillard (Sep 19 2022 at 09:37):

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...

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

view this post on Zulip Théo Zimmermann (Sep 19 2022 at 10:54):

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

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

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

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

view this post on Zulip Théo Zimmermann (Sep 19 2022 at 12:31):

No idea, but clearly that's the thing to debug. I'll try to look into it.

view this post on Zulip Théo Zimmermann (Sep 19 2022 at 14:11):

I think I know what the problem is.

view this post on Zulip Théo Zimmermann (Sep 19 2022 at 14:14):

Yes.

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

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

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

view this post on Zulip Matthieu Sozeau (Sep 19 2022 at 14:35):

It looks fine

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

view this post on Zulip Théo Zimmermann (Sep 19 2022 at 18:55):

LGTM


Last updated: Jan 29 2023 at 15:02 UTC