From 822a449b230adb821fb5aef3af1e75bb7fa30057 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Sun, 23 Feb 2025 16:19:04 +0100 Subject: [PATCH] coqPackages.mathcomp*: update stdlib dependencies --- .../coq-modules/fourcolor/default.nix | 2 -- .../coq-modules/hierarchy-builder/default.nix | 2 +- .../coq-modules/jasmin/default.nix | 2 ++ .../coq-modules/mathcomp-analysis/default.nix | 33 +++++++------------ .../coq-modules/mathcomp-finmap/default.nix | 3 +- .../mathcomp-real-closed/default.nix | 2 -- .../coq-modules/mathcomp-tarjan/default.nix | 2 -- .../coq-modules/mathcomp-word/default.nix | 2 ++ .../coq-modules/mathcomp/default.nix | 5 ++- .../coq-modules/odd-order/default.nix | 2 -- 10 files changed, 20 insertions(+), 35 deletions(-) diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix index 6b3b169f8d2b0..39f6b75135eb3 100644 --- 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 index 33105a0f89b32..0402beec1cb2e 100644 --- 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 index 16a1a15eb9e11..6b143bbd8d512 100644 --- 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 index a3e128c686dac..9264c12f1bd50 100644 --- 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 index db0a28594d8c1..fe408966797bb 100644 --- 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 index 722df10efe7bd..7654c47abf081 100644 --- 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 index a681e9fb23478..9246a0b0682e2 100644 --- 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 index 84a3345e70660..6175ae80538ec 100644 --- 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 index 5bc97ccade5f6..9958d1732ee1c 100644 --- 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 index 76a09f6d2bc1b..1e4e044ae558f 100644 --- 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; {