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.
This commit is contained in:
Théo Zimmermann 2021-08-16 22:38:17 +02:00
parent c93884185a
commit 90654cce7d
No known key found for this signature in database
GPG key ID: F1744A0942F536C7
3 changed files with 12 additions and 2 deletions

View file

@ -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. * `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"`, * `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. * `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. * `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. * `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`, * `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`,

View file

@ -27,6 +27,7 @@ in
dropDerivationAttrs ? [], dropDerivationAttrs ? [],
useDune2ifVersion ? (x: false), useDune2ifVersion ? (x: false),
useDune2 ? false, useDune2 ? false,
opam-name ? "coq-${pname}",
... ...
}@args: }@args:
let let
@ -34,7 +35,7 @@ let
"version" "fetcher" "repo" "owner" "domain" "releaseRev" "version" "fetcher" "repo" "owner" "domain" "releaseRev"
"displayVersion" "defaultVersion" "useMelquiondRemake" "displayVersion" "defaultVersion" "useMelquiondRemake"
"release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix" "release" "extraBuildInputs" "extraPropagatedBuildInputs" "namePrefix"
"meta" "useDune2ifVersion" "useDune2" "meta" "useDune2ifVersion" "useDune2" "opam-name"
"extraInstallFlags" "setCOQBIN" "mlPlugin" "extraInstallFlags" "setCOQBIN" "mlPlugin"
"dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs; "dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
fetch = import ../coq/meta-fetch/default.nix fetch = import ../coq/meta-fetch/default.nix
@ -90,9 +91,14 @@ stdenv.mkDerivation (removeAttrs ({
extraInstallFlags; extraInstallFlags;
}) })
// (optionalAttrs useDune2 { // (optionalAttrs useDune2 {
buildPhase = ''
runHook preBuild
dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
runHook postBuild
'';
installPhase = '' installPhase = ''
runHook preInstall runHook preInstall
dune install --prefix=$out dune install ${opam-name} --prefix=$out
mv $out/lib/coq $out/lib/TEMPORARY mv $out/lib/coq $out/lib/TEMPORARY
mkdir $out/lib/coq/ mkdir $out/lib/coq/
mv $out/lib/TEMPORARY $out/lib/coq/${coq.coq-version} mv $out/lib/TEMPORARY $out/lib/coq/${coq.coq-version}

View file

@ -4,7 +4,10 @@ with lib; mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "multinomials"; pname = "multinomials";
opam-name = "coq-mathcomp-multinomials";
owner = "math-comp"; owner = "math-comp";
inherit version; inherit version;
defaultVersion = with versions; switch [ coq.version mathcomp.version ] [ defaultVersion = with versions; switch [ coq.version mathcomp.version ] [
{ cases = [ (range "8.10" "8.13") "1.12.0" ]; out = "1.5.4"; } { cases = [ (range "8.10" "8.13") "1.12.0" ]; out = "1.5.4"; }