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.

3 files changed, 41 insertions, 14 deletions

diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix
index 8d86602bf38e..03922303ee34 100644
--- a/pkgs/build-support/coq/default.nix
+++ b/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)
diff --git a/pkgs/build-support/coq/meta-fetch/default.nix b/pkgs/build-support/coq/meta-fetch/default.nix
index b01ae72a2089..e7b15af4f06e 100644
--- a/pkgs/build-support/coq/meta-fetch/default.nix
+++ b/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;
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index 4958ad893e92..dfa6a63571fd 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 }:
+  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; }