coqPackages.mkCoqDerivation: rely on namePrefix to compute default opam-name

As suggested by Cyril Cohen in https://github.com/NixOS/nixpkgs/pull/134362#discussion_r698379405.
This commit is contained in:
Théo Zimmermann 2021-09-07 14:44:40 +02:00 committed by Vincent Laporte
parent e331c30a72
commit 20291381c1
3 changed files with 4 additions and 6 deletions

View file

@ -28,12 +28,12 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
* `domain` (optional, defaults to `"github.com"`), domains including the strings `"github"` or `"gitlab"` in their names are automatically supported, otherwise, one must change the `fetcher` argument to support them (cf `pkgs/development/coq-modules/heq/default.nix` for an example), * `domain` (optional, defaults to `"github.com"`), domains including the strings `"github"` or `"gitlab"` in their names are automatically supported, otherwise, one must change the `fetcher` argument to support them (cf `pkgs/development/coq-modules/heq/default.nix` for an example),
* `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags, * `releaseRev` (optional, defaults to `(v: v)`), provides a default mapping from release names to revision hashes/branch names/tags,
* `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers, * `displayVersion` (optional), provides a way to alter the computation of `name` from `pname`, by explaining how to display version numbers,
* `namePrefix` (optional), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`, * `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
* `extraBuildInputs` (optional), by default `buildInputs` just contains `coq`, this allows to add more build inputs, * `extraBuildInputs` (optional), by default `buildInputs` just contains `coq`, this allows to add more build inputs,
* `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. * `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. * `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

@ -16,7 +16,7 @@ in
displayVersion ? {}, displayVersion ? {},
release ? {}, release ? {},
extraBuildInputs ? [], extraBuildInputs ? [],
namePrefix ? [], namePrefix ? [ "coq" ],
enableParallelBuilding ? true, enableParallelBuilding ? true,
extraInstallFlags ? [], extraInstallFlags ? [],
setCOQBIN ? true, setCOQBIN ? true,
@ -27,7 +27,7 @@ in
dropDerivationAttrs ? [], dropDerivationAttrs ? [],
useDune2ifVersion ? (x: false), useDune2ifVersion ? (x: false),
useDune2 ? false, useDune2 ? false,
opam-name ? "coq-${pname}", opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
... ...
}@args: }@args:
let let
@ -44,7 +44,6 @@ let
location = { inherit domain owner repo; }; location = { inherit domain owner repo; };
} // optionalAttrs (args?fetcher) {inherit fetcher;}); } // optionalAttrs (args?fetcher) {inherit fetcher;});
fetched = fetch (if !isNull version then version else defaultVersion); fetched = fetch (if !isNull version then version else defaultVersion);
namePrefix = args.namePrefix or [ "coq" ];
display-pkg = n: sep: v: display-pkg = n: sep: v:
let d = displayVersion.${n} or (if sep == "" then ".." else true); in let d = displayVersion.${n} or (if sep == "" then ".." else true); in
n + optionalString (v != "" && v != null) (switch d [ n + optionalString (v != "" && v != null) (switch d [

View file

@ -4,7 +4,6 @@ with lib; mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ]; namePrefix = [ "coq" "mathcomp" ];
pname = "multinomials"; pname = "multinomials";
opam-name = "coq-mathcomp-multinomials";
owner = "math-comp"; owner = "math-comp";