diff options
11 files changed, 21 insertions, 21 deletions
diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md index 38bf7db1850..6a5c72cb0a9 100644 --- a/doc/languages-frameworks/coq.section.md +++ b/doc/languages-frameworks/coq.section.md @@ -31,7 +31,7 @@ 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`, -* `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune2`, `useDune2ifVersion` and `mlPlugin` are set). +* `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune`, `useDuneifVersion` and `mlPlugin` are set). * `extraNativeBuildInputs` (optional, deprecated), an additional list of derivation to add to `nativeBuildInputs`, * `overrideNativeBuildInputs` (optional) replaces the default list of derivation to which `nativeBuildInputs` and `extraNativeBuildInputs` adds extra elements, * `buildInputs` (optional), is a list of libraries and dependencies that are required to build and run the current derivation, in addition to the default one `[ coq ]`, @@ -39,8 +39,8 @@ The recommended way of defining a derivation for a Coq library, is to use the `c * `overrideBuildInputs` (optional) replaces the default list of derivation to which `buildInputs` and `extraBuildInputs` adds extras elements, * `propagatedBuildInputs` (optional) is passed as is to `mkDerivation`, we recommend to use this for Coq libraries and Coq plugin dependencies, as this makes sure the paths of the compiled libraries and plugins will always be added to the build environements of subsequent derivation, which is necessary for Coq packages to work correctly, * `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 `nativeBuildInputs`, `buildInputs`, and `propagatedBuildInputs` 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. `useDune2ifVersion = 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. +* `useDuneifVersion` (optional, default to `(x: false)` uses Dune to build the package if the provided predicate evaluates to true on the version, e.g. `useDuneifVersion = versions.isGe "1.1"` will use dune if the version of the package is greater or equal to `"1.1"`, +* `useDune` (optional, defaults to `false`) uses Dune to build the package if set to true, the presence of this attribute overrides the behavior of the previous one. * `opam-name` (optional, defaults to concatenating with a dash separator the components of `namePrefix` and `pname`), name of the Dune package to build. * `enableParallelBuilding` (optional, defaults to `true`), since it is activated by default, we provide a way to disable it. * `extraInstallFlags` (optional), allows to extend `installFlags` which initializes the variable `COQMF_COQLIB` so as to install in the proper subdirectory. Indeed Coq libraries should be installed in `$(out)/lib/coq/${coq.coq-version}/user-contrib/`. Such directories are automatically added to the `$COQPATH` environment variable by the hook defined in the Coq derivation. diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix index 0dc5c999ea3..e0ba7b3e08c 100644 --- a/pkgs/build-support/coq/default.nix +++ b/pkgs/build-support/coq/default.nix @@ -30,8 +30,8 @@ in dropAttrs ? [], keepAttrs ? [], dropDerivationAttrs ? [], - useDune2ifVersion ? (x: false), - useDune2 ? false, + useDuneifVersion ? (x: false), + useDune ? false, opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])), ... }@args: @@ -44,7 +44,7 @@ let "extraBuildInputs" "extraNativeBuildInputs" "overrideBuildInputs" "overrideNativeBuildInputs" "namePrefix" - "meta" "useDune2ifVersion" "useDune2" "opam-name" + "meta" "useDuneifVersion" "useDune" "opam-name" "extraInstallFlags" "setCOQBIN" "mlPlugin" "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs; fetch = import ../coq/meta-fetch/default.nix @@ -65,7 +65,7 @@ let ] "") + optionalString (v == null) "-broken"; append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-"; prefix-name = foldl append-version "" namePrefix; - useDune2 = args.useDune2 or (useDune2ifVersion fetched.version); + useDune = args.useDune or (useDuneifVersion fetched.version); coqlib-flags = switch coq.coq-version [ { case = v: versions.isLe "8.6" v && v != "dev" ; out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; } @@ -85,8 +85,8 @@ stdenv.mkDerivation (removeAttrs ({ nativeBuildInputs = args.overrideNativeBuildInputs or ([ which coq.ocamlPackages.findlib ] - ++ optional useDune2 coq.ocamlPackages.dune_2 - ++ optional (useDune2 || mlPlugin) coq.ocamlPackages.ocaml + ++ optional useDune coq.ocamlPackages.dune_3 + ++ optional (useDune || mlPlugin) coq.ocamlPackages.ocaml ++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs); buildInputs = args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or []) ++ extraBuildInputs); @@ -107,7 +107,7 @@ stdenv.mkDerivation (removeAttrs ({ coqlib-flags ++ docdir-flags ++ extraInstallFlags; }) -// (optionalAttrs useDune2 { +// (optionalAttrs useDune { buildPhase = '' runHook preBuild dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES} diff --git a/pkgs/development/coq-modules/addition-chains/default.nix b/pkgs/development/coq-modules/addition-chains/default.nix index 8de9a8e411c..63ba0e80507 100644 --- a/pkgs/development/coq-modules/addition-chains/default.nix +++ b/pkgs/development/coq-modules/addition-chains/default.nix @@ -19,7 +19,7 @@ mkCoqDerivation { propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra mathcomp-fingroup paramcoq ]; - useDune2 = true; + useDune = true; meta = { description = "Exponentiation algorithms following addition chains"; diff --git a/pkgs/development/coq-modules/coqide/default.nix b/pkgs/development/coq-modules/coqide/default.nix index a827057a118..4e1f9e5f666 100644 --- a/pkgs/development/coq-modules/coqide/default.nix +++ b/pkgs/development/coq-modules/coqide/default.nix @@ -22,7 +22,7 @@ with lib; mkCoqDerivation rec { ''; prefixKey = "-prefix "; - useDune2 = true; + useDune = true; buildInputs = [ copyDesktopItems diff --git a/pkgs/development/coq-modules/gaia-hydras/default.nix b/pkgs/development/coq-modules/gaia-hydras/default.nix index ce254aff78b..5377600caba 100644 --- a/pkgs/development/coq-modules/gaia-hydras/default.nix +++ b/pkgs/development/coq-modules/gaia-hydras/default.nix @@ -21,7 +21,7 @@ with lib; mkCoqDerivation rec { mathcomp-zify ]; - useDune2 = true; + useDune = true; meta = { description = "Comparison between ordinals in Gaia and Hydra battles"; diff --git a/pkgs/development/coq-modules/hydra-battles/default.nix b/pkgs/development/coq-modules/hydra-battles/default.nix index d59afa53ac3..2729f7c2139 100644 --- a/pkgs/development/coq-modules/hydra-battles/default.nix +++ b/pkgs/development/coq-modules/hydra-battles/default.nix @@ -16,7 +16,7 @@ with lib; { case = range "8.11" "8.12"; out = "0.4"; } ] null; - useDune2 = true; + useDune = true; meta = { description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq"; diff --git a/pkgs/development/coq-modules/mathcomp-word/default.nix b/pkgs/development/coq-modules/mathcomp-word/default.nix index f39fbe0ac6a..69735c801ed 100644 --- a/pkgs/development/coq-modules/mathcomp-word/default.nix +++ b/pkgs/development/coq-modules/mathcomp-word/default.nix @@ -6,7 +6,7 @@ mkCoqDerivation { pname = "word"; owner = "jasmin-lang"; repo = "coqword"; - useDune2 = true; + useDune = true; releaseRev = v: "v${v}"; diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix index 8144d87b9fb..57f4a381b20 100644 --- a/pkgs/development/coq-modules/multinomials/default.nix +++ b/pkgs/development/coq-modules/multinomials/default.nix @@ -1,5 +1,5 @@ { coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough, - lib, version ? null, useDune2 ? false }@args: + lib, version ? null, useDune ? false }@args: with lib; mkCoqDerivation { namePrefix = [ "coq" "mathcomp" ]; @@ -31,7 +31,7 @@ with lib; mkCoqDerivation { "1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m"; }; - useDune2ifVersion = v: versions.isGe "1.5.3" v || v == "dev"; + useDuneifVersion = v: versions.isGe "1.5.3" v || v == "dev"; preConfigure = '' patchShebangs configure || true @@ -45,4 +45,4 @@ with lib; mkCoqDerivation { license = licenses.cecill-c; }; } -// optionalAttrs (args?useDune2) { inherit useDune2; } +// optionalAttrs (args?useDune) { inherit useDune; } diff --git a/pkgs/development/coq-modules/serapi/default.nix b/pkgs/development/coq-modules/serapi/default.nix index 7c3b656da91..e3ec9bfdc39 100644 --- a/pkgs/development/coq-modules/serapi/default.nix +++ b/pkgs/development/coq-modules/serapi/default.nix @@ -27,7 +27,7 @@ in { case = isEq "8.10"; out = "8.10.0+0.7.2"; } ] null; - useDune2 = true; + useDune = true; patches = [ ./janestreet-0.15.patch ]; diff --git a/pkgs/development/coq-modules/topology/default.nix b/pkgs/development/coq-modules/topology/default.nix index 37585eea8c7..eb94912307a 100644 --- a/pkgs/development/coq-modules/topology/default.nix +++ b/pkgs/development/coq-modules/topology/default.nix @@ -25,7 +25,7 @@ mkCoqDerivation rec { propagatedBuildInputs = [ zorns-lemma ]; - useDune2ifVersion = versions.isGe "9.0"; + useDuneifVersion = versions.isGe "9.0"; meta = { description = "General topology in Coq"; diff --git a/pkgs/development/coq-modules/zorns-lemma/default.nix b/pkgs/development/coq-modules/zorns-lemma/default.nix index b003e15891d..10f238ae6c1 100644 --- a/pkgs/development/coq-modules/zorns-lemma/default.nix +++ b/pkgs/development/coq-modules/zorns-lemma/default.nix @@ -25,7 +25,7 @@ with lib; { case = "8.5"; out = "8.5.0"; } ] null; - useDune2ifVersion = versions.isGe "9.0"; + useDuneifVersion = versions.isGe "9.0"; meta = { description = "Development of basic set theory"; |