coqPackages.multinomials: 1.5.2 -> 1.5.4 (#115427)

- This is the first packages which uses Dune in order to build and install
  so I had to refactor build-support/coq/default.nix in order to support it.
- I added a new feature: one can now release.v.sha256 empty to try to download
  with a fake sha256, hence failures are reported and one can copy paste the
  sha256 given by the error message.
- I updated the documentation of languages-frameworks/coq.section.md accordingly.

doc/languages-frameworks/coq.section.md

@@ -21,8 +21,8 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
   * if it is a string of the form `owner:branch` then it tries to download the `branch` of owner `owner` for a project of the same name using the same vcs, and the `version` attribute of the resulting derivation is set to `"dev"`, additionally if the owner is not provided (i.e. if the `owner:` prefix is missing), it defaults to the original owner of the package (see below),
   * if it is a string of the form `"#N"`, and the domain is github, then it tries to download the current head of the pull request `#N` from github,
 * `defaultVersion` (optional). Coq libraries may be compatible with some specific versions of Coq only. The `defaultVersion` attribute is used when no `version` is provided (or if `version = null`) to select the version of the library to use by default, depending on the context. This selection will mainly depend on a `coq` version number but also possibly on other packages versions (e.g. `mathcomp`). If its value ends up to be `null`, the package is marked for removal in end-user `coqPackages` attribute set.
-* `release` (optional, defaults to `{}`), lists all the known releases of the library and for each of them provides an attribute set with at least a `sha256` attribute (you may use the shell command `nix-prefetch-url --unpack <archive-url>` to find it, where `<archive-url>` is for example `https://github.com/owner/repo/archive/version.tar.gz`), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.`domain`, `owner`, `repo`, `rev` assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. `version` and `src`).
-* `fetcher` (optional, default to a generic fetching mechanism supporting github or gitlab based infrastructures), is a function that takes at least an `owner`, a `repo`, a `rev`, and a `sha256` and returns an attribute set with a `version` and `src`.
+* `release` (optional, defaults to `{}`), lists all the known releases of the library and for each of them provides an attribute set with at least a `sha256` attribute (you may put the empty string `""` in order to automatically insert a fake sha256, this will trigger an error which will allow you to find the correct sha256), each attribute set of the list of releases also takes optional overloading arguments for the fetcher as below (i.e.`domain`, `owner`, `repo`, `rev` assuming the default fetcher is used) and optional overrides for the result of the fetcher (i.e. `version` and `src`).
+* `fetcher` (optional, defaults to a generic fetching mechanism supporting github or gitlab based infrastructures), is a function that takes at least an `owner`, a `repo`, a `rev`, and a `sha256` and returns an attribute set with a `version` and `src`.
 * `repo` (optional, defaults to the value of `pname`),
 * `owner` (optional, defaults to `"coq-community"`).
 * `domain` (optional, defaults to `"github.com"`), domains including the strings `"github"` or `"gitlab"` in their names are automatically supported, otherwise, one must change the `fetcher` argument to support them (cf `pkgs/development/coq-modules/heq/default.nix` for an example),
@@ -31,6 +31,8 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
 * `namePrefix` (optional), 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,
 * `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.
 * `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.
 * `setCOQBIN` (optional, defaults to `true`), by default, the environment variable `$COQBIN` is set to the current Coq's binary, but one can disable this behavior by setting it to `false`,

pkgs/build-support/coq/default.nix

@@ -25,13 +25,16 @@ in
   dropAttrs ? [],
   keepAttrs ? [],
   dropDerivationAttrs ? [],
+  useDune2ifVersion ? (x: false),
+  useDune2 ? false,
   ...
 }@args:
 let
   args-to-remove = foldl (flip remove) ([
     "version" "fetcher" "repo" "owner" "domain" "releaseRev"
     "displayVersion" "defaultVersion" "useMelquiondRemake"
-    "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix" "meta"
+    "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
+    "meta" "useDune2ifVersion" "useDune2"
     "extraInstallFlags" "setCOQBIN" "mlPlugin"
     "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
   fetch = import ../coq/meta-fetch/default.nix
@@ -54,6 +57,7 @@ let
   append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
   prefix-name = foldl append-version "" namePrefix;
   var-coqlib-install = (optionalString (versions.isGe "8.7" coq.coq-version) "COQMF_") + "COQLIB";
+  useDune2 = args.useDune2 or useDune2ifVersion fetched.version;
 in
 
 stdenv.mkDerivation (removeAttrs ({
@@ -62,7 +66,10 @@ stdenv.mkDerivation (removeAttrs ({
 
   inherit (fetched) version src;
 
-  buildInputs = [ coq ] ++ optionals mlPlugin coq.ocamlBuildInputs ++ extraBuildInputs;
+  buildInputs = [ coq ]
+    ++ optionals mlPlugin coq.ocamlBuildInputs
+    ++ optionals useDune2 [coq.ocaml coq.ocamlPackages.dune_2]
+    ++ extraBuildInputs;
   inherit enableParallelBuilding;
 
   meta = ({ platforms = coq.meta.platforms; } //
@@ -73,20 +80,30 @@ stdenv.mkDerivation (removeAttrs ({
     optionalAttrs (fetched.broken or false) { coqFilter = true; broken = true; }) //
     (args.meta or {}) ;
 
-} //
-(optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; }) //
-(optionalAttrs (!args?installPhase && !args?useMelquiondRemake) {
+}
+// (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; })
+// (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) {
   installFlags =
     [ "${var-coqlib-install}=$(out)/lib/coq/${coq.coq-version}/" ] ++
     optional (match ".*doc$" (args.installTargets or "") != null)
       "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ++
     extraInstallFlags;
-}) //
-(optionalAttrs (args?useMelquiondRemake) rec {
+})
+// (optionalAttrs useDune2 {
+  installPhase = ''
+    runHook preInstall
+    dune install --prefix=$out
+    mv $out/lib/coq $out/lib/TEMPORARY
+    mkdir $out/lib/coq/
+    mv $out/lib/TEMPORARY $out/lib/coq/${coq.coq-version}
+    runHook postInstall
+  '';
+})
+// (optionalAttrs (args?useMelquiondRemake) rec {
   COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib";
   preConfigurePhases = "autoconf";
   configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ];
   buildPhase = "./remake -j$NIX_BUILD_CORES";
   installPhase = "./remake install";
-}) //
-(removeAttrs args args-to-remove)) dropDerivationAttrs)
+})
+// (removeAttrs args args-to-remove)) dropDerivationAttrs)

pkgs/build-support/coq/meta-fetch/default.nix

@@ -39,10 +39,13 @@ switch arg [
   { case = isPathString; out = { version = "dev"; src = arg; }; }
   { case = pred.union isVersion isShortVersion;
     out = let v = if isVersion arg then arg else shortVersion arg; in
-      if !release.${v}?sha256 then throw "meta-fetch: a sha256 must be provided for each release"
-      else {
-        version = release.${v}.version or v;
-        src = release.${v}.src or fetcher (location // { rev = releaseRev v; } // release.${v});
+      let
+        given-sha256 = release.${v}.sha256 or "";
+        sha256 = if given-sha256 == "" then lib.fakeSha256 else given-sha256;
+        rv = release.${v} // { inherit sha256; }; in
+      {
+        version = rv.version or v;
+        src = rv.src or fetcher (location // { rev = releaseRev v; } // rv);
       };
     }
   { case = isString;

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

@@ -1,5 +1,5 @@
 { coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
-  lib, version ? null }:
+  lib, version ? null, useDune2 ? false }@args:
 with lib; mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
@@ -7,12 +7,16 @@ with lib; mkCoqDerivation {
   owner = "math-comp";
   inherit version;
   defaultVersion =  with versions; switch [ coq.version mathcomp.version ] [
+      { cases = [ (range "8.10" "8.13") "1.12.0" ];             out = "1.5.4"; }
+      { cases = [ (range "8.10" "8.12") "1.12.0" ];             out = "1.5.3"; }
       { cases = [ (range "8.7" "8.12")  "1.11.0" ];             out = "1.5.2"; }
       { cases = [ (range "8.7" "8.11")  (range "1.8" "1.10") ]; out = "1.5.0"; }
       { cases = [ (range "8.7" "8.10")  (range "1.8" "1.10") ]; out = "1.4"; }
       { cases = [ "8.6"                 (range "1.6" "1.7") ];  out = "1.1"; }
     ] null;
   release = {
+    "1.5.4".sha256 = "0s4sbh4y88l125hdxahr56325hdhxxdmqmrz7vv8524llyv3fciq";
+    "1.5.3".sha256 = "1462x40y2qydjd2wcg8r6qr8cx3xv4ixzh2h8vp9h7arylkja1qd";
     "1.5.2".sha256 = "15aspf3jfykp1xgsxf8knqkxv8aav2p39c2fyirw7pwsfbsv2c4s";
     "1.5.1".sha256 = "13nlfm2wqripaq671gakz5mn4r0xwm0646araxv0nh455p9ndjs3";
     "1.5.0".sha256 = "064rvc0x5g7y1a0nip6ic91vzmq52alf6in2bc2dmss6dmzv90hw";
@@ -24,6 +28,8 @@ with lib; mkCoqDerivation {
     "1.0".sha256   = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
   };
 
+  useDune2ifVersion = versions.isGe "1.5.3";
+
   propagatedBuildInputs =
     [ mathcomp.ssreflect mathcomp.algebra mathcomp-finmap mathcomp-bigenough ];
 
@@ -32,3 +38,4 @@ with lib; mkCoqDerivation {
     license = licenses.cecill-c;
   };
 }
+// optionalAttrs (args?useDune2) { inherit useDune2; }