coqPackages.mathcomp: remove Stdlib dependency

Adapting to https://github.com/math-comp/math-comp/pull/1343
2025-02-14 14:21:56 +01:00
parent e18836ceaa
commit c407726f4f
15 changed files with 45 additions and 10 deletions
@@ -3,6 +3,7 @@
  mkCoqDerivation,
  coq,
  mathcomp-ssreflect,
+  stdlib,
  version ? null,
 }:

@@ -33,7 +34,7 @@ mkCoqDerivation {
      }
    ] null;

-  propagatedBuildInputs = [ mathcomp-ssreflect ];
+  propagatedBuildInputs = [ mathcomp-ssreflect stdlib ];

  meta = with lib; {
    homepage = "https://www.ps.uni-saarland.de/autosubst/";
@@ -3,6 +3,8 @@
  mkCoqDerivation,
  coq,
  mathcomp,
+  mathcomp-algebra-tactics,
+  stdlib,
  version ? null,
 }:

@@ -35,7 +37,7 @@ mkCoqDerivation {
  release."1.1.0".sha256 = "sha256-TCw1kSXeW0ysIdLeNr+EGmpGumEE9i8tinEMp57UXaE=";
  release."1.0.0".sha256 = "0nv5mdgrd075dpd8bc7h0xc5i95v0pkm0bfyq5rj6ii1s54dwcjl";

-  propagatedBuildInputs = [ mathcomp.algebra ];
+  propagatedBuildInputs = [ mathcomp.algebra mathcomp-algebra-tactics stdlib ];

  meta = with lib; {
    description = "Formalization of bitset operations in Coq";
@@ -27,7 +27,6 @@ default-elpi-version = if elpi-version != null then elpi-version else (
 elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
 propagatedBuildInputs_wo_elpi = [
  coq.ocamlPackages.findlib
-  stdlib
 ];
 derivation = mkCoqDerivation {
  pname = "elpi";
@@ -120,4 +119,12 @@ patched-derivation2 = patched-derivation1.overrideAttrs
        propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.ppx_optcomp ];
      }
  );
-in patched-derivation2
+patched-derivation3 = patched-derivation2.overrideAttrs
+  (
+    o:
+    lib.optionalAttrs (o.version != null && o.version == "2.4.0")
+      {
+        propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
+      }
+  );
+in patched-derivation3
@@ -3,6 +3,7 @@
  mkCoqDerivation,
  autoconf,
  coq,
+  stdlib,
  ssreflect,
  version ? null,
 }:
@@ -56,7 +57,7 @@ mkCoqDerivation {
  releaseRev = v: "coquelicot-${v}";

  nativeBuildInputs = [ autoconf ];
-  propagatedBuildInputs = [ ssreflect ];
+  propagatedBuildInputs = [ stdlib ssreflect ];
  useMelquiondRemake.logpath = "Coquelicot";

  meta = with lib; {
@@ -4,6 +4,7 @@
  coq,
  version ? null,
  ssreflect,
+  stdlib,
 }:

 mkCoqDerivation {
@@ -47,7 +48,7 @@ mkCoqDerivation {
  release."0.1.1".sha256 = "sha256-Gu8aInLxTXfAFE0/gWRYI046Dx3Gv1j1+gx92v/UnPI=";
  release."0.1.0".sha256 = "sha256:11crnjm8hyis1qllkks3d7r07s1rfzwvyvpijya3s6iqfh8c7xwh";

-  propagatedBuildInputs = [ ssreflect ];
+  propagatedBuildInputs = [ ssreflect stdlib ];

  mlPlugin = true;

@@ -3,6 +3,7 @@
  mkCoqDerivation,
  coq,
  mathcomp,
+  stdlib,
  version ? null,
 }:

@@ -67,6 +68,7 @@ mkCoqDerivation {
    mathcomp.algebra
    mathcomp.ssreflect
    mathcomp.fingroup
+    stdlib
  ];

  meta = with lib; {
@@ -3,6 +3,7 @@
  mkCoqDerivation,
  coq,
  mathcomp,
+  stdlib,
  version ? null,
 }:

@@ -52,6 +53,7 @@ mkCoqDerivation {
    mathcomp.ssreflect
    mathcomp.algebra
    mathcomp.fingroup
+    stdlib
  ];

  meta = with lib; {
@@ -4,6 +4,7 @@
  coq,
  mathcomp,
  mathcomp-finmap,
+  mathcomp-algebra-tactics,
  fourcolor,
  hierarchy-builder,
  version ? null,
@@ -68,6 +69,7 @@ mkCoqDerivation {
    mathcomp.algebra
    mathcomp-finmap
    mathcomp.fingroup
+    mathcomp-algebra-tactics
    fourcolor
    hierarchy-builder
  ];
@@ -2,6 +2,7 @@
  coq,
  mkCoqDerivation,
  mathcomp,
+  stdlib,
  lib,
  version ? null,
 }:
@@ -107,7 +108,7 @@ mkCoqDerivation {
    "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
  };

-  propagatedBuildInputs = [ mathcomp.ssreflect ];
+  propagatedBuildInputs = [ mathcomp.ssreflect stdlib ];

  meta = {
    description = "Finset and finmap library";
@@ -3,6 +3,7 @@
  mkCoqDerivation,
  mathcomp,
  mathcomp-bigenough,
+  stdlib,
  lib,
  version ? null,
 }:
@@ -115,6 +116,7 @@ mkCoqDerivation {
    mathcomp.fingroup
    mathcomp.solvable
    mathcomp-bigenough
+    stdlib
  ];

  meta = {
@@ -3,6 +3,7 @@
  mkCoqDerivation,
  mathcomp-ssreflect,
  mathcomp-fingroup,
+  stdlib,
  lib,
  version ? null,
 }@args:
@@ -52,6 +53,7 @@ mkCoqDerivation {
  propagatedBuildInputs = [
    mathcomp-ssreflect
    mathcomp-fingroup
+    stdlib
  ];

  meta = {
@@ -5,6 +5,7 @@
  mathcomp-algebra,
  mathcomp-ssreflect,
  mathcomp-fingroup,
+  stdlib,
  version ? null,
 }:

@@ -56,6 +57,7 @@ mkCoqDerivation rec {
    mathcomp-algebra
    mathcomp-ssreflect
    mathcomp-fingroup
+    stdlib
  ];

  meta = {
@@ -136,13 +136,20 @@ let
        installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
      }
    );
-    patched-derivation = patched-derivation2.overrideAttrs (o:
+    patched-derivation3 = patched-derivation2.overrideAttrs (o:
      lib.optionalAttrs (o.version != null
        && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
      {
        propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
      }
    );
-    in patched-derivation;
+    patched-derivation4 = patched-derivation3.overrideAttrs (o:
+      lib.optionalAttrs (o.version != null
+        && lib.versions.isLe "2.3.0" o.version)
+      {
+        propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
+      }
+    );
+    in patched-derivation4;
 in
 mathcomp_ (if single then "single" else "all")
@@ -2,6 +2,7 @@
  lib,
  mkCoqDerivation,
  mathcomp,
+  stdlib,
  version ? null,
 }:

@@ -45,6 +46,7 @@ mkCoqDerivation {
    mathcomp.solvable
    mathcomp.field
    mathcomp.all
+    stdlib
  ];

  meta = with lib; {
@@ -3,6 +3,7 @@
  mkCoqDerivation,
  coq,
  mathcomp,
+  stdlib,
  version ? null,
 }:

@@ -46,7 +47,7 @@ mkCoqDerivation {
      ]
      null;

-  propagatedBuildInputs = [ mathcomp.ssreflect ];
+  propagatedBuildInputs = [ mathcomp.ssreflect stdlib ];

  meta = with lib; {
    description = "Regular Language Representations in Coq";