diff --git a/doc/languages-frameworks/coq.section.md b/doc/languages-frameworks/coq.section.md index 11777b5eef42..80d8566f804f 100644 --- a/doc/languages-frameworks/coq.section.md +++ b/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`. diff --git a/pkgs/build-support/coq/default.nix b/pkgs/build-support/coq/default.nix index 52ef17f05c00..2a078a55d695 100644 --- a/pkgs/build-support/coq/default.nix +++ b/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 { diff --git a/pkgs/development/coq-modules/hierarchy-builder/default.nix b/pkgs/development/coq-modules/hierarchy-builder/default.nix index fb7de66f16e6..3eb5b4d476f5 100644 --- a/pkgs/development/coq-modules/hierarchy-builder/default.nix +++ b/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; } )