coqPackages.mathcomp*: update stdlib dependencies

NixOS · Feb 24, 2025 · 822a449 · 822a449
1 parent b07c16e
commit 822a449
Show file tree

Hide file tree

Showing 10 changed files with 20 additions and 35 deletions.
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -3,7 +3,6 @@
   mkCoqDerivation,
   coq,
   mathcomp,
-  stdlib,
   version ? null,
 }:
 
@@ -68,7 +67,6 @@ mkCoqDerivation {
     mathcomp.algebra
     mathcomp.ssreflect
     mathcomp.fingroup
-    stdlib
   ];
 
   meta = with lib; {

diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -49,6 +49,6 @@ hb.overrideAttrs (o:
    else
    { installFlags = [ "VFILES=structures.v" ] ++ o.installFlags; })
   //
-  lib.optionalAttrs (lib.versions.isLe "1.8.1" o.version)
+  lib.optionalAttrs (o.version != null && o.version == "1.8.1")
     { propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ]; }
 )
diff --git a/pkgs/development/coq-modules/jasmin/default.nix b/pkgs/development/coq-modules/jasmin/default.nix
@@ -3,6 +3,7 @@
   mkCoqDerivation,
   coq,
   mathcomp,
+  mathcomp-algebra-tactics,
   mathcomp-word,
   version ? null,
 }:
@@ -23,6 +24,7 @@ mkCoqDerivation {
   release."2024.07.2".sha256 = "sha256-aF8SYY5jRxQ6iEr7t6mRN3BEmIDhJ53PGhuZiJGB+i8=";
 
   propagatedBuildInputs = [
+    mathcomp-algebra-tactics
     mathcomp-word
   ];
 

diff --git a/pkgs/development/coq-modules/mathcomp-analysis/default.nix b/pkgs/development/coq-modules/mathcomp-analysis/default.nix
@@ -5,6 +5,7 @@
   mathcomp-finmap,
   mathcomp-bigenough,
   hierarchy-builder,
+  stdlib,
   single ? false,
   coqPackages,
   coq,
@@ -176,26 +177,11 @@ let
       ];
       intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
       pkgpath = lib.switch package [
-        {
-          case = "single";
-          out = ".";
-        }
-        {
-          case = "analysis";
-          out = "theories";
-        }
-        {
-          case = "experimental-reals";
-          out = "experimental_reals";
-        }
-        {
-          case = "reals-stdlib";
-          out = "reals_stdlib";
-        }
-        {
-          case = "analysis-stdlib";
-          out = "analysis_stdlib";
-        }
+        { case = "single"; out = "."; }
+        { case = "analysis"; out = "theories"; }
+        { case = "experimental-reals"; out = "experimental_reals"; }
+        { case = "reals-stdlib"; out = "reals_stdlib"; }
+        { case = "analysis-stdlib"; out = "analysis_stdlib"; }
       ] package;
       pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
       derivation = mkCoqDerivation ({
@@ -226,7 +212,12 @@ let
           ++ lib.optionals (lib.elem package [
             "analysis"
             "single"
-          ]) analysis-deps;
+          ]) analysis-deps
+          ++ lib.optional (lib.elem package [
+            "reals-stdlib"
+            "analysis-stdlib"
+            "single"
+          ]) stdlib;
 
         preBuild = ''
           cd ${pkgpath}

diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix
@@ -2,7 +2,6 @@
   coq,
   mkCoqDerivation,
   mathcomp,
-  stdlib,
   lib,
   version ? null,
 }:
@@ -108,7 +107,7 @@ mkCoqDerivation {
     "1.0.0".sha256 = "0sah7k9qm8sw17cgd02f0x84hki8vj8kdz7h15i7rmz08rj0whpa";
   };
 
-  propagatedBuildInputs = [ mathcomp.ssreflect stdlib ];
+  propagatedBuildInputs = [ mathcomp.ssreflect ];
 
   meta = {
     description = "Finset and finmap library";

diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@@ -3,7 +3,6 @@
   mkCoqDerivation,
   mathcomp,
   mathcomp-bigenough,
-  stdlib,
   lib,
   version ? null,
 }:
@@ -116,7 +115,6 @@ mkCoqDerivation {
     mathcomp.fingroup
     mathcomp.solvable
     mathcomp-bigenough
-    stdlib
   ];
 
   meta = {

diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix
@@ -3,7 +3,6 @@
   mkCoqDerivation,
   mathcomp-ssreflect,
   mathcomp-fingroup,
-  stdlib,
   lib,
   version ? null,
 }@args:
@@ -53,7 +52,6 @@ mkCoqDerivation {
   propagatedBuildInputs = [
     mathcomp-ssreflect
     mathcomp-fingroup
-    stdlib
   ];
 
   meta = {

diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix
@@ -3,6 +3,7 @@
   coq,
   mkCoqDerivation,
   mathcomp,
+  stdlib,
   lib,
   version ? null,
 }:
@@ -80,6 +81,7 @@ mkCoqDerivation {
     mathcomp.algebra
     mathcomp.ssreflect
     mathcomp.fingroup
+    stdlib
   ];
 
   meta = with lib; {

diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -80,7 +80,7 @@ let
         mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
         nativeBuildInputs = lib.optionals withDoc [ graphviz lua ];
         buildInputs = [ ncurses ];
-        propagatedBuildInputs = [ stdlib ] ++ mathcomp-deps;
+        propagatedBuildInputs = mathcomp-deps;
 
         buildFlags = lib.optional withDoc "doc";
 
@@ -144,8 +144,7 @@ let
       }
     );
     patched-derivation4 = patched-derivation3.overrideAttrs (o:
-      lib.optionalAttrs (o.version != null
-        && lib.versions.isLe "2.3.0" o.version)
+      lib.optionalAttrs (o.version != null && o.version == "2.3.0")
       {
         propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
       }

diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
@@ -2,7 +2,6 @@
   lib,
   mkCoqDerivation,
   mathcomp,
-  stdlib,
   version ? null,
 }:
 
@@ -46,7 +45,6 @@ mkCoqDerivation {
     mathcomp.solvable
     mathcomp.field
     mathcomp.all
-    stdlib
   ];
 
   meta = with lib; {