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

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

doc/languages-frameworks/coq.section.md

@@ -29,7 +29,8 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
 * `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags,
 * `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers,
 * `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
-* `extraBuildInputs` (optional), by default `buildInputs` just contains `coq`, this allows to add more build inputs,
+* `extraNativeBuildInputs` (optional), by default `nativeBuildInputs` just contains `coq`, this allows to add more native build inputs, `nativeBuildInputs` are executables and `buildInputs` are libraries and dependencies,
+* `extraBuildInputs` (optional), this allows to add more build inputs,
 * `mlPlugin` (optional, defaults to `false`). Some extensions (plugins) might require OCaml and sometimes other OCaml packages. Standard dependencies can be added by setting the current option to `true`. For a finer grain control, the `coq.ocamlPackages` attribute can be used in `extraBuildInputs` to depend on the same package set Coq was built against.
 * `useDune2ifVersion` (optional, default to `(x: false)` uses Dune2 to build the package if the provided predicate evaluates to true on the version, e.g. `useDune2if = versions.isGe "1.1"`  will use dune if the version of the package is greater or equal to `"1.1"`,
 * `useDune2` (optional, defaults to `false`) uses Dune2 to build the package if set to true, the presence of this attribute overrides the behavior of the previous one.

pkgs/applications/science/logic/coq/default.nix

@@ -81,7 +81,7 @@ self = stdenv.mkDerivation {
 
   passthru = {
     inherit coq-version;
-    inherit ocamlPackages ocamlBuildInputs;
+    inherit ocamlPackages ocamlBuildInputs ocamlNativeBuildInputs;
     # For compatibility
     inherit (ocamlPackages) ocaml camlp5 findlib num ;
     emacsBufferSetup = pkgs: ''

pkgs/build-support/coq/default.nix

@@ -16,6 +16,7 @@ in
   displayVersion ? {},
   release ? {},
   extraBuildInputs ? [],
+  extraNativeBuildInputs ? [],
   namePrefix ? [ "coq" ],
   enableParallelBuilding ? true,
   extraInstallFlags ? [],
@@ -34,7 +35,7 @@ let
   args-to-remove = foldl (flip remove) ([
     "version" "fetcher" "repo" "owner" "domain" "releaseRev"
     "displayVersion" "defaultVersion" "useMelquiondRemake"
-    "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
+    "release" "extraBuildInputs" "extraNativeBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
     "meta" "useDune2ifVersion" "useDune2" "opam-name"
     "extraInstallFlags" "setCOQBIN" "mlPlugin"
     "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
@@ -67,9 +68,11 @@ stdenv.mkDerivation (removeAttrs ({
 
   inherit (fetched) version src;
 
-  buildInputs = [ coq ]
-    ++ optionals mlPlugin coq.ocamlBuildInputs
+  nativeBuildInputs = [ coq ]
     ++ optionals useDune2 [coq.ocaml coq.ocamlPackages.dune_2]
+    ++ optionals mlPlugin coq.ocamlNativeBuildInputs
+    ++ extraNativeBuildInputs;
+  buildInputs = optionals mlPlugin coq.ocamlBuildInputs
     ++ extraBuildInputs;
   inherit enableParallelBuilding;
 

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;

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;
 

pkgs/development/coq-modules/coq-bits/default.nix

@@ -22,6 +22,7 @@ with lib; mkCoqDerivation {
     };
   };
 
+  extraBuildInputs = [ mathcomp.ssreflect mathcomp.fingroup ];
   propagatedBuildInputs = [ mathcomp.algebra ];
 
   installPhase = ''

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.";

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;

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";
 

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 ];
 

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 ";

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";

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";

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";

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 ];
 

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;

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 = {

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";

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";

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";

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";
 

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";

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";

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

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;