From c407726f4fbbe6a6c88a78a532ecb47fd9f10e88 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Fri, 14 Feb 2025 10:10:52 +0100 Subject: [PATCH] coqPackages.mathcomp: remove Stdlib dependency Adapting to https://github.com/math-comp/math-comp/pull/1343 --- pkgs/development/coq-modules/autosubst/default.nix | 3 ++- pkgs/development/coq-modules/coq-bits/default.nix | 4 +++- pkgs/development/coq-modules/coq-elpi/default.nix | 11 +++++++++-- pkgs/development/coq-modules/coquelicot/default.nix | 3 ++- pkgs/development/coq-modules/deriving/default.nix | 3 ++- pkgs/development/coq-modules/fourcolor/default.nix | 2 ++ pkgs/development/coq-modules/gaia/default.nix | 2 ++ pkgs/development/coq-modules/graph-theory/default.nix | 2 ++ .../coq-modules/mathcomp-finmap/default.nix | 3 ++- .../coq-modules/mathcomp-real-closed/default.nix | 2 ++ .../coq-modules/mathcomp-tarjan/default.nix | 2 ++ .../development/coq-modules/mathcomp-zify/default.nix | 2 ++ pkgs/development/coq-modules/mathcomp/default.nix | 11 +++++++++-- pkgs/development/coq-modules/odd-order/default.nix | 2 ++ pkgs/development/coq-modules/reglang/default.nix | 3 ++- 15 files changed, 45 insertions(+), 10 deletions(-) diff --git a/pkgs/development/coq-modules/autosubst/default.nix b/pkgs/development/coq-modules/autosubst/default.nix index ce28e4a0d911..415756ad2dcb 100644 --- a/pkgs/development/coq-modules/autosubst/default.nix +++ b/pkgs/development/coq-modules/autosubst/default.nix @@ -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/"; diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix index 6754ba4d66a7..bdf4e0714f26 100644 --- a/pkgs/development/coq-modules/coq-bits/default.nix +++ b/pkgs/development/coq-modules/coq-bits/default.nix @@ -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"; diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix index 927f9d282131..5c0f9d2a6e9e 100644 --- a/pkgs/development/coq-modules/coq-elpi/default.nix +++ b/pkgs/development/coq-modules/coq-elpi/default.nix @@ -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 diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix index 806d7d1304b9..c26fc70c7ba3 100644 --- a/pkgs/development/coq-modules/coquelicot/default.nix +++ b/pkgs/development/coq-modules/coquelicot/default.nix @@ -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; { diff --git a/pkgs/development/coq-modules/deriving/default.nix b/pkgs/development/coq-modules/deriving/default.nix index 259cf724c316..aa9a802b4bf5 100644 --- a/pkgs/development/coq-modules/deriving/default.nix +++ b/pkgs/development/coq-modules/deriving/default.nix @@ -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; diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix index 39f6b75135eb..6b3b169f8d2b 100644 --- a/pkgs/development/coq-modules/fourcolor/default.nix +++ b/pkgs/development/coq-modules/fourcolor/default.nix @@ -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; { diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix index 05079005b6c0..6110407c94e7 100644 --- a/pkgs/development/coq-modules/gaia/default.nix +++ b/pkgs/development/coq-modules/gaia/default.nix @@ -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; { diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix index 6ef59a006de5..1f0b0eb41f28 100644 --- a/pkgs/development/coq-modules/graph-theory/default.nix +++ b/pkgs/development/coq-modules/graph-theory/default.nix @@ -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 ]; diff --git a/pkgs/development/coq-modules/mathcomp-finmap/default.nix b/pkgs/development/coq-modules/mathcomp-finmap/default.nix index fe408966797b..db0a28594d8c 100644 --- a/pkgs/development/coq-modules/mathcomp-finmap/default.nix +++ b/pkgs/development/coq-modules/mathcomp-finmap/default.nix @@ -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"; diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix index 7654c47abf08..722df10efe7b 100644 --- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix +++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix @@ -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 = { diff --git a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix index 9246a0b0682e..a681e9fb2347 100644 --- a/pkgs/development/coq-modules/mathcomp-tarjan/default.nix +++ b/pkgs/development/coq-modules/mathcomp-tarjan/default.nix @@ -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 = { diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix index ec0c7cdcaa95..fe2535af6cf9 100644 --- a/pkgs/development/coq-modules/mathcomp-zify/default.nix +++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix @@ -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 = { diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix index c4442ba1283c..5bc97ccade5f 100644 --- a/pkgs/development/coq-modules/mathcomp/default.nix +++ b/pkgs/development/coq-modules/mathcomp/default.nix @@ -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") diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix index 1e4e044ae558..76a09f6d2bc1 100644 --- a/pkgs/development/coq-modules/odd-order/default.nix +++ b/pkgs/development/coq-modules/odd-order/default.nix @@ -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; { diff --git a/pkgs/development/coq-modules/reglang/default.nix b/pkgs/development/coq-modules/reglang/default.nix index cd0513a6e02a..9b4fd8efea59 100644 --- a/pkgs/development/coq-modules/reglang/default.nix +++ b/pkgs/development/coq-modules/reglang/default.nix @@ -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";