coqPackages.mkCoqDerivation: upgrade to Dune 3

And remove the version number from the corresponding attributes.

11 files changed, 21 insertions, 21 deletions

diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md
index 38bf7db18506b..6a5c72cb0a943 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 0dc5c999ea357..e0ba7b3e08c8c 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 8de9a8e411cd8..63ba0e8050721 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 a827057a118b6..4e1f9e5f66628 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 ce254aff78bb4..5377600caba42 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 d59afa53ac311..2729f7c213918 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 f39fbe0ac6a6b..69735c801edd8 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 8144d87b9fbf4..57f4a381b2049 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 7c3b656da9138..e3ec9bfdc39ac 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 37585eea8c79f..eb94912307a7f 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 b003e15891d48..10f238ae6c110 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";