BoomMicrophone/nixpkgs-suyu
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity

mkCoqDerivation: do not set DESTDIR

Browse source 
Fixes #178109
This commit is contained in:
Vincent Laporte 2022-06-18 10:56:48 +02:00
parent a5051e29e2
commit af888339b6
No known key found for this signature in database
GPG key ID: EBD582ADDDB1F81F
3 changed files with 5 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
doc/languages-frameworks/coq.section.md
View file

@ -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`.

2
pkgs/build-support/coq/default.nix
View file

@ -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 {

3
pkgs/development/coq-modules/hierarchy-builder/default.nix
View file

@ -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; }
)