diff options
25 files changed, 54 insertions, 35 deletions
diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md index a5155aedaf5..9a692104a04 100644 --- a/doc/languages-frameworks/coq.section.md +++ b/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. diff --git a/pkgs/applications/science/logic/coq/default.nix b/pkgs/applications/science/logic/coq/default.nix index e9cc106017d..c88bd0421ca 100644 --- a/pkgs/applications/science/logic/coq/default.nix +++ b/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: '' diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix index 569b07cded6..a681bbda557 100644 --- a/pkgs/build-support/coq/default.nix +++ b/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; 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; |