From 90654cce7d17ea5485efd5489673bb34f7578d45 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Th=C3=A9o=20Zimmermann?= <theo.zimmermann@inria.fr>
Date: Mon, 16 Aug 2021 22:38:17 +0200
Subject: [PATCH] coqPackages.mkCoqDerivation: fix useDune2

- Reuse build phase from the `buildDunePackage` function.
- Only install the package that was just built (useful for monorepo support).
- Introduces `opam-name` to override the default package name to build with Dune.
---
 doc/languages-frameworks/coq.section.md               |  1 +
 pkgs/build-support/coq/default.nix                    | 10 ++++++++--
 pkgs/development/coq-modules/multinomials/default.nix |  3 +++
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md
index 0674c5a4702e..39b60d83ac7d 100644
--- a/doc/languages-frameworks/coq.section.md
+++ b/doc/languages-frameworks/coq.section.md
@@ -33,6 +33,7 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
 * `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.
+* `opam-name` (optional, defaults to `coq-` followed by the value of `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.
 * `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`,
diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix
index ba300f2f8cf5..5f2b5e646b0b 100644
--- a/pkgs/build-support/coq/default.nix
+++ b/pkgs/build-support/coq/default.nix
@@ -27,6 +27,7 @@ in
   dropDerivationAttrs ? [],
   useDune2ifVersion ? (x: false),
   useDune2 ? false,
+  opam-name ? "coq-${pname}",
   ...
 }@args:
 let
@@ -34,7 +35,7 @@ let
     "version" "fetcher" "repo" "owner" "domain" "releaseRev"
     "displayVersion" "defaultVersion" "useMelquiondRemake"
     "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
-    "meta" "useDune2ifVersion" "useDune2"
+    "meta" "useDune2ifVersion" "useDune2" "opam-name"
     "extraInstallFlags" "setCOQBIN" "mlPlugin"
     "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
   fetch = import ../coq/meta-fetch/default.nix
@@ -90,9 +91,14 @@ stdenv.mkDerivation (removeAttrs ({
     extraInstallFlags;
 })
 // (optionalAttrs useDune2 {
+  buildPhase = ''
+    runHook preBuild
+    dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
+    runHook postBuild
+  '';
   installPhase = ''
     runHook preInstall
-    dune install --prefix=$out
+    dune install ${opam-name} --prefix=$out
     mv $out/lib/coq $out/lib/TEMPORARY
     mkdir $out/lib/coq/
     mv $out/lib/TEMPORARY $out/lib/coq/${coq.coq-version}
diff --git a/pkgs/development/coq-modules/multinomials/default.nix b/pkgs/development/coq-modules/multinomials/default.nix
index dfa6a63571fd..acbb602a54ef 100644
--- a/pkgs/development/coq-modules/multinomials/default.nix
+++ b/pkgs/development/coq-modules/multinomials/default.nix
@@ -4,7 +4,10 @@ with lib; mkCoqDerivation {
 
   namePrefix = [ "coq" "mathcomp" ];
   pname = "multinomials";
+  opam-name = "coq-mathcomp-multinomials";
+
   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"; }