Merge pull request #178131 from vbgl/coq-fix-issue-178109

mkCoqDerivation: do not set DESTDIR

doc/languages-frameworks/coq.section.md

@@ -41,7 +41,7 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
 * `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 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 variables `DESTDIR` and `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.
+* `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`,
 * `useMelquiondRemake` (optional, default to `null`) is an attribute set, which, if given, overloads the `preConfigurePhases`, `configureFlags`, `buildPhase`, and `installPhase` attributes of the derivation for a specific use in libraries using `remake` as set up by Guillaume Melquiond for `flocq`, `gappalib`, `interval`, and `coquelicot` (see the corresponding derivation for concrete examples of use of this option). For backward compatibility, the attribute `useMelquiondRemake.logpath` must be set to the logical root of the library (otherwise, one can pass `useMelquiondRemake = {}` to activate this without backward compatibility).
 * `dropAttrs`, `keepAttrs`, `dropDerivationAttrs` are all optional and allow to tune which attribute is added or removed from the final call to `mkDerivation`.

pkgs/build-support/coq/default.nix

@@ -104,7 +104,7 @@ stdenv.mkDerivation (removeAttrs ({
 // (optionalAttrs setCOQBIN { COQBIN = "${coq}/bin/"; })
 // (optionalAttrs (!args?installPhase && !args?useMelquiondRemake) {
   installFlags =
-    [ "DESTDIR=$(out)" ] ++ coqlib-flags ++ docdir-flags ++
+    coqlib-flags ++ docdir-flags ++
     extraInstallFlags;
 })
 // (optionalAttrs useDune2 {

pkgs/development/coq-modules/hierarchy-builder/default.nix

@@ -32,4 +32,7 @@ with lib; let hb = mkCoqDerivation {
 hb.overrideAttrs (o:
   optionalAttrs (versions.isGe "1.2.0" o.version || o.version == "dev")
     { buildPhase = "make build"; }
+  //
+  optionalAttrs (versions.isGe "1.1.0" o.version || o.version == "dev")
+  { installFlags = [ "DESTDIR=$(out)" ] ++ o.installFlags; }
 )