coqPackages: tree-wide move packages to nativeBuildInputs and add strictDeps = true

Co-authored-by: Vincent Laporte <vbgl@users.noreply.github.com>

22 files changed, 45 insertions, 30 deletions

diff --git a/pkgs/development/coq-modules/QuickChick/default.nix b/pkgs/development/coq-modules/QuickChick/default.nix
index fcaaaac615e..56ce94ecc6f 100644
--- a/pkgs/development/coq-modules/QuickChick/default.nix
+++ b/pkgs/development/coq-modules/QuickChick/default.nix
@@ -34,10 +34,10 @@ mkCoqDerivation {
     "substituteInPlace Makefile --replace quickChickTool.byte quickChickTool.native";
 
   mlPlugin = true;
+  extraNativeBuildInputs = lib.optional recent coq.ocamlPackages.ocamlbuild;
   extraBuildInputs = lib.optional recent coq.ocamlPackages.num;
   propagatedBuildInputs = [ ssreflect ]
-    ++ lib.optionals recent [ coq-ext-lib simple-io ]
-    ++ lib.optional recent coq.ocamlPackages.ocamlbuild;
+    ++ lib.optionals recent [ coq-ext-lib simple-io ];
   extraInstallFlags = [ "-f Makefile.coq" ];
 
   enableParallelBuilding = false;
diff --git a/pkgs/development/coq-modules/addition-chains/default.nix b/pkgs/development/coq-modules/addition-chains/default.nix
index c6b6f79bf01..8a0248c952c 100644
--- a/pkgs/development/coq-modules/addition-chains/default.nix
+++ b/pkgs/development/coq-modules/addition-chains/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, paramcoq
+{ lib, mkCoqDerivation, coq, mathcomp-ssreflect, mathcomp-algebra, mathcomp-fingroup, paramcoq
 , version ? null }:
 with lib;
 
@@ -17,7 +17,7 @@ mkCoqDerivation {
     { case = range "8.11" "8.12"; out = "0.4"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra paramcoq ];
+  propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra mathcomp-fingroup paramcoq ];
 
   useDune2 = true;
 
diff --git a/pkgs/development/coq-modules/coq-bits/default.nix b/pkgs/development/coq-modules/coq-bits/default.nix
index 1da0a0d17ea..6cb6bb3c813 100644
--- a/pkgs/development/coq-modules/coq-bits/default.nix
+++ b/pkgs/development/coq-modules/coq-bits/default.nix
@@ -22,6 +22,7 @@ with lib; mkCoqDerivation {
     };
   };
 
+  extraBuildInputs = [ mathcomp.ssreflect mathcomp.fingroup ];
   propagatedBuildInputs = [ mathcomp.algebra ];
 
   installPhase = ''
diff --git a/pkgs/development/coq-modules/coq-elpi/default.nix b/pkgs/development/coq-modules/coq-elpi/default.nix
index c4055648c5a..55423047caa 100644
--- a/pkgs/development/coq-modules/coq-elpi/default.nix
+++ b/pkgs/development/coq-modules/coq-elpi/default.nix
@@ -48,9 +48,8 @@ in mkCoqDerivation {
   release."1.6.0".sha256      = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
   releaseRev = v: "v${v}";
 
-  nativeBuildInputs = [ which ];
+  extraNativeBuildInputs = [ which elpi ];
   mlPlugin = true;
-  extraBuildInputs = [ elpi ];
 
   meta = {
     description = "Coq plugin embedding ELPI.";
diff --git a/pkgs/development/coq-modules/coqtail-math/default.nix b/pkgs/development/coq-modules/coqtail-math/default.nix
index 891d1fae62c..c9c3915414c 100644
--- a/pkgs/development/coq-modules/coqtail-math/default.nix
+++ b/pkgs/development/coq-modules/coqtail-math/default.nix
@@ -10,7 +10,7 @@ mkCoqDerivation {
   release."20201124".rev    = "5c22c3d7dcd8cf4c47cf84a281780f5915488e9e";
   release."20201124".sha256 = "sha256-wd+Lh7dpAD4zfpyKuztDmSFEZo5ZiFrR8ti2jUCVvoQ=";
 
-  buildInputs = with coq.ocamlPackages; [ ocaml findlib ];
+  extraNativeBuildInputs = with coq.ocamlPackages; [ ocaml findlib ];
 
   meta = {
     license = licenses.lgpl3Only;
diff --git a/pkgs/development/coq-modules/coquelicot/default.nix b/pkgs/development/coq-modules/coquelicot/default.nix
index b7f5802b9d4..1a6dba9b0c0 100644
--- a/pkgs/development/coq-modules/coquelicot/default.nix
+++ b/pkgs/development/coq-modules/coquelicot/default.nix
@@ -16,7 +16,7 @@ with lib; mkCoqDerivation {
   release."3.0.2".sha256 = "1rqfbbskgz7b1bcpva8wh3v3456sq2364y804f94sc8y5sij23nl";
   releaseRev = v: "coquelicot-${v}";
 
-  nativeBuildInputs = [ which autoconf ];
+  extraNativeBuildInputs = [ which autoconf ];
   propagatedBuildInputs = [ ssreflect ];
   useMelquiondRemake.logpath = "Coquelicot";
 
diff --git a/pkgs/development/coq-modules/dpdgraph/default.nix b/pkgs/development/coq-modules/dpdgraph/default.nix
index 82fb6c536d3..7cf6132bf6a 100644
--- a/pkgs/development/coq-modules/dpdgraph/default.nix
+++ b/pkgs/development/coq-modules/dpdgraph/default.nix
@@ -39,7 +39,7 @@ mkCoqDerivation {
   release."0.6".sha256   = "0qvar8gfbrcs9fmvkph5asqz4l5fi63caykx3bsn8zf0xllkwv0n";
   releaseRev = v: "v${v}";
 
-  nativeBuildInputs = [ autoreconfHook ];
+  extraNativeBuildInputs = [ autoreconfHook ];
   mlPlugin = true;
   extraBuildInputs = [ coq.ocamlPackages.ocamlgraph ];
 
diff --git a/pkgs/development/coq-modules/fourcolor/default.nix b/pkgs/development/coq-modules/fourcolor/default.nix
index 19d35b4c97e..a9c5d021077 100644
--- a/pkgs/development/coq-modules/fourcolor/default.nix
+++ b/pkgs/development/coq-modules/fourcolor/default.nix
@@ -16,7 +16,7 @@ mkCoqDerivation {
     { cases = [ (isLe "8.13") (pred.inter (isGe "1.11.0") (isLt "1.13")) ]; out = "1.2.3"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp.algebra ];
+  propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
 
   meta = {
     description = "Formal proof of the Four Color Theorem ";
diff --git a/pkgs/development/coq-modules/gaia/default.nix b/pkgs/development/coq-modules/gaia/default.nix
index c7c64c9d257..53c317db87c 100644
--- a/pkgs/development/coq-modules/gaia/default.nix
+++ b/pkgs/development/coq-modules/gaia/default.nix
@@ -15,7 +15,7 @@ with lib; mkCoqDerivation {
   ] null;
 
   propagatedBuildInputs =
-    [ mathcomp.ssreflect mathcomp.algebra ];
+    [ mathcomp.ssreflect mathcomp.algebra mathcomp.fingroup ];
 
   meta = {
     description = "Implementation of books from Bourbaki's Elements of Mathematics in Coq";
diff --git a/pkgs/development/coq-modules/gappalib/default.nix b/pkgs/development/coq-modules/gappalib/default.nix
index 440c9395a37..02905dcffed 100644
--- a/pkgs/development/coq-modules/gappalib/default.nix
+++ b/pkgs/development/coq-modules/gappalib/default.nix
@@ -12,7 +12,7 @@ with lib; mkCoqDerivation {
   release."1.4.4".sha256 = "114q2hgw64j6kqa9mg3qcp1nlf0ia46z2xadq81fnkxqm856ml7l";
   releaseRev = v: "gappalib-coq-${v}";
 
-  nativeBuildInputs = [ which autoconf ];
+  extraNativeBuildInputs = [ which autoconf ];
   mlPlugin = true;
   propagatedBuildInputs = [ flocq ];
   useMelquiondRemake.logpath = "Gappa";
diff --git a/pkgs/development/coq-modules/graph-theory/default.nix b/pkgs/development/coq-modules/graph-theory/default.nix
index 6374ede7970..eedbe6fb5d8 100644
--- a/pkgs/development/coq-modules/graph-theory/default.nix
+++ b/pkgs/development/coq-modules/graph-theory/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-finmap, mathcomp-fingroup
 , hierarchy-builder, version ? null }:
 
 with lib;
@@ -15,7 +15,7 @@ mkCoqDerivation {
     { case = range "8.13" "8.14"; out = "0.9"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap hierarchy-builder ];
+  propagatedBuildInputs = [ mathcomp-algebra mathcomp-finmap mathcomp-fingroup hierarchy-builder ];
 
   meta = {
     description = "Library of formalized graph theory results in Coq";
diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix
index 1f5a616bb54..c0fa2d7c8e0 100644
--- a/pkgs/development/coq-modules/hierarchy-builder/default.nix
+++ b/pkgs/development/coq-modules/hierarchy-builder/default.nix
@@ -17,7 +17,7 @@ with lib; let hb = mkCoqDerivation {
   release."0.10.0".sha256 = "1a3vry9nzavrlrdlq3cys3f8kpq3bz447q8c4c7lh2qal61wb32h";
   releaseRev = v: "v${v}";
 
-  nativeBuildInputs = [ which ];
+  extraNativeBuildInputs = [ which ];
 
   propagatedBuildInputs = [ coq-elpi ];
 
diff --git a/pkgs/development/coq-modules/interval/default.nix b/pkgs/development/coq-modules/interval/default.nix
index b608f3d0205..b9257d415e5 100644
--- a/pkgs/development/coq-modules/interval/default.nix
+++ b/pkgs/development/coq-modules/interval/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, bignums ? null, gnuplot_qt, version ? null }:
+{ lib, mkCoqDerivation, which, autoconf, coq, coquelicot, flocq, mathcomp-ssreflect, mathcomp-fingroup, bignums ? null, gnuplot_qt, version ? null }:
 
 mkCoqDerivation rec {
   pname = "interval";
@@ -20,8 +20,8 @@ mkCoqDerivation rec {
   release."3.3.0".sha256 = "0lz2hgggzn4cvklvm8rpaxvwaryf37i8mzqajqgdxdbd8f12acsz";
   releaseRev = v: "interval-${v}";
 
-  nativeBuildInputs = [ which autoconf ];
-  propagatedBuildInputs = [ bignums coquelicot flocq ]
+  extraNativeBuildInputs = [ which autoconf ];
+  propagatedBuildInputs = [ bignums coquelicot flocq mathcomp-ssreflect mathcomp-fingroup ]
     ++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
   useMelquiondRemake.logpath = "Interval";
   mlPlugin = true;
diff --git a/pkgs/development/coq-modules/itauto/default.nix b/pkgs/development/coq-modules/itauto/default.nix
index 843a99de4be..af535993362 100644
--- a/pkgs/development/coq-modules/itauto/default.nix
+++ b/pkgs/development/coq-modules/itauto/default.nix
@@ -13,7 +13,7 @@ mkCoqDerivation rec {
   ] null;
 
   mlPlugin = true;
-  extraBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
   enableParallelBuilding = false;
 
   meta = {
diff --git a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
index 0f0937d1e45..0364ad09578 100644
--- a/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-real-closed/default.nix
@@ -24,7 +24,14 @@ with lib; mkCoqDerivation {
       { cases = [ (isGe "8.7")   "1.7.0"  ]; out = "1.0.1"; }
     ] null;
 
-  propagatedBuildInputs = [ mathcomp.ssreflect mathcomp.field mathcomp-bigenough ];
+  propagatedBuildInputs = [
+    mathcomp.ssreflect
+    mathcomp.algebra
+    mathcomp.field
+    mathcomp.fingroup
+    mathcomp.solvable
+    mathcomp-bigenough
+  ];
 
   meta = {
     description = "Mathematical Components Library on real closed fields";
diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix
index 67f4c4ef786..9c74edd5471 100644
--- a/pkgs/development/coq-modules/mathcomp-word/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-word/default.nix
@@ -17,7 +17,7 @@ mkCoqDerivation {
     { cases = [ (range "8.12" "8.14") (isGe "1.12") ]; out = "1.0"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp.algebra ];
+  propagatedBuildInputs = [ mathcomp.algebra mathcomp.ssreflect mathcomp.fingroup ];
 
   meta = {
     description = "Yet Another Coq Library on Machine Words";
diff --git a/pkgs/development/coq-modules/mathcomp-zify/default.nix b/pkgs/development/coq-modules/mathcomp-zify/default.nix
index ce2bd98f3d0..2e2593669f3 100644
--- a/pkgs/development/coq-modules/mathcomp-zify/default.nix
+++ b/pkgs/development/coq-modules/mathcomp-zify/default.nix
@@ -1,4 +1,4 @@
-{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
+{ lib, mkCoqDerivation, coq, mathcomp-algebra, mathcomp-ssreflect,  mathcomp-fingroup, version ? null }:
 
 with lib; mkCoqDerivation rec {
   namePrefix = [ "coq" "mathcomp" ];
@@ -15,7 +15,7 @@ with lib; mkCoqDerivation rec {
   release."1.0.0+1.12+8.13".sha256 = "1j533vx6lacr89bj1bf15l1a0s7rvrx4l00wyjv99aczkfbz6h6k";
   release."1.1.0+1.12+8.13".sha256 = "1plf4v6q5j7wvmd5gsqlpiy0vwlw6hy5daq2x42gqny23w9mi2pr";
 
-  propagatedBuildInputs = [ mathcomp-algebra ];
+  propagatedBuildInputs = [ mathcomp-algebra mathcomp-ssreflect mathcomp-fingroup ];
 
   meta = {
     description = "Micromega tactics for Mathematical Components";
diff --git a/pkgs/development/coq-modules/mathcomp/default.nix b/pkgs/development/coq-modules/mathcomp/default.nix
index 5b41d62d775..0f562fec287 100644
--- a/pkgs/development/coq-modules/mathcomp/default.nix
+++ b/pkgs/development/coq-modules/mathcomp/default.nix
@@ -59,10 +59,9 @@ let
       derivation = mkCoqDerivation ({
         inherit version pname defaultVersion release releaseRev repo owner;
 
-        nativeBuildInputs = optionals withDoc [ graphviz lua ];
         mlPlugin = versions.isLe "8.6" coq.coq-version;
-        extraBuildInputs = [ ncurses which ];
-        propagatedBuildInputs = mathcomp-deps;
+        extraNativeBuildInputs = [ which ] ++ optionals withDoc [ graphviz lua ];
+        extraBuildInputs = [ ncurses ] ++ mathcomp-deps;
 
         buildFlags = optional withDoc "doc";
 
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index a74ee17f1c6..8144d87b9fb 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -38,7 +38,7 @@ with lib; mkCoqDerivation {
   '';
 
   propagatedBuildInputs =
-    [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
+    [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp.fingroup mathcomp-bigenough ];
 
   meta = {
     description = "A Coq/SSReflect Library for Monoidal Rings and Multinomials";
diff --git a/pkgs/development/coq-modules/odd-order/default.nix b/pkgs/development/coq-modules/odd-order/default.nix
index 20090340633..0d2005326c5 100644
--- a/pkgs/development/coq-modules/odd-order/default.nix
+++ b/pkgs/development/coq-modules/odd-order/default.nix
@@ -16,7 +16,15 @@ mkCoqDerivation {
     { case = (range "1.10.0" "1.12.0"); out = "1.12.0"; }
   ] null;
 
-  propagatedBuildInputs = [ mathcomp.character ];
+  propagatedBuildInputs = [
+    mathcomp.character
+    mathcomp.ssreflect
+    mathcomp.fingroup
+    mathcomp.algebra
+    mathcomp.solvable
+    mathcomp.field
+    mathcomp.all
+  ];
 
   meta = {
     description = "Formal proof of the Odd Order Theorem";
diff --git a/pkgs/development/coq-modules/semantics/default.nix b/pkgs/development/coq-modules/semantics/default.nix
index 9b8bb10a5f2..89567d401b2 100644
--- a/pkgs/development/coq-modules/semantics/default.nix
+++ b/pkgs/development/coq-modules/semantics/default.nix
@@ -24,7 +24,8 @@ mkCoqDerivation rec {
   ] null;
 
   mlPlugin = true;
-  extraBuildInputs = (with coq.ocamlPackages; [ num ocamlbuild ]);
+  extraNativeBuildInputs = (with coq.ocamlPackages; [ ocamlbuild ]);
+  extraBuildInputs = (with coq.ocamlPackages; [ num ]);
 
   postPatch = ''
     for p in Make Makefile.coq.local
diff --git a/pkgs/development/coq-modules/simple-io/default.nix b/pkgs/development/coq-modules/simple-io/default.nix
index 3631bdd54bf..693ff2b01d6 100644
--- a/pkgs/development/coq-modules/simple-io/default.nix
+++ b/pkgs/development/coq-modules/simple-io/default.nix
@@ -7,7 +7,7 @@ with lib; mkCoqDerivation {
   inherit version;
   defaultVersion = if versions.range "8.7" "8.13" coq.coq-version then "1.3.0" else null;
   release."1.3.0".sha256 = "1yp7ca36jyl9kz35ghxig45x6cd0bny2bpmy058359p94wc617ax";
-  extraBuildInputs = (with coq.ocamlPackages; [ ocaml ocamlbuild ]);
+  extraNativeBuildInputs = (with coq.ocamlPackages; [ ocaml ocamlbuild ]);
   propagatedBuildInputs = [ coq-ext-lib ];
 
   doCheck = true;