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.

2 files changed, 33 insertions, 13 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;