colin/nixpkgs
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

coqPackages.mkCoqDerivation: upgrade to Dune 3

Browse Source 
And remove the version number from the corresponding attributes.
This commit is contained in:
Théo Zimmermann 2022-10-01 16:42:29 +02:00 committed by Vincent Laporte
parent faacb60b6e
commit 2dc3552aa1
11 changed files with 21 additions and 21 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
doc/languages-frameworks/coq.section.md
View File

@ -31,7 +31,7 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
* `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,
* `namePrefix` (optional, defaults to `[ "coq" ]`), provides a way to alter the computation of `name` from `pname`, by explaining which dependencies must occur in `name`,
* `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune2`, `useDune2ifVersion` and `mlPlugin` are set).
* `nativeBuildInputs` (optional), is a list of executables that are required to build the current derivation, in addition to the default ones (namely `which`, `dune` and `ocaml` depending on whether `useDune`, `useDuneifVersion` and `mlPlugin` are set).
* `extraNativeBuildInputs` (optional, deprecated), an additional list of derivation to add to `nativeBuildInputs`,
* `overrideNativeBuildInputs` (optional) replaces the default list of derivation to which `nativeBuildInputs` and `extraNativeBuildInputs` adds extra elements,
* `buildInputs` (optional), is a list of libraries and dependencies that are required to build and run the current derivation, in addition to the default one `[ coq ]`,
@ -39,8 +39,8 @@ The recommended way of defining a derivation for a Coq library, is to use the `c
* `overrideBuildInputs` (optional) replaces the default list of derivation to which `buildInputs` and `extraBuildInputs` adds extras elements,
* `propagatedBuildInputs` (optional) is passed as is to `mkDerivation`, we recommend to use this for Coq libraries and Coq plugin dependencies, as this makes sure the paths of the compiled libraries and plugins will always be added to the build environements of subsequent derivation, which is necessary for Coq packages to work correctly,
* `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 `nativeBuildInputs`, `buildInputs`, and `propagatedBuildInputs` 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. `useDune2ifVersion = 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.
* `useDuneifVersion` (optional, default to `(x: false)` uses Dune to build the package if the provided predicate evaluates to true on the version, e.g. `useDuneifVersion = versions.isGe "1.1"` will use dune if the version of the package is greater or equal to `"1.1"`,
* `useDune` (optional, defaults to `false`) uses Dune 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 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.

14
pkgs/build-support/coq/default.nix
View File

@ -30,8 +30,8 @@ in
dropAttrs ? [],
keepAttrs ? [],
dropDerivationAttrs ? [],
useDune2ifVersion ? (x: false),
useDune2 ? false,
useDuneifVersion ? (x: false),
useDune ? false,
opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
...
}@args:
@ -44,7 +44,7 @@ let
"extraBuildInputs" "extraNativeBuildInputs"
"overrideBuildInputs" "overrideNativeBuildInputs"
"namePrefix"
"meta" "useDune2ifVersion" "useDune2" "opam-name"
"meta" "useDuneifVersion" "useDune" "opam-name"
"extraInstallFlags" "setCOQBIN" "mlPlugin"
"dropAttrs" "dropDerivationAttrs" "keepAttrs" ] ++ dropAttrs) keepAttrs;
fetch = import ../coq/meta-fetch/default.nix
@ -65,7 +65,7 @@ let
] "") + optionalString (v == null) "-broken";
append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
prefix-name = foldl append-version "" namePrefix;
useDune2 = args.useDune2 or (useDune2ifVersion fetched.version);
useDune = args.useDune or (useDuneifVersion fetched.version);
coqlib-flags = switch coq.coq-version [
{ case = v: versions.isLe "8.6" v && v != "dev" ;
out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ]; }
@ -85,8 +85,8 @@ stdenv.mkDerivation (removeAttrs ({
nativeBuildInputs = args.overrideNativeBuildInputs
or ([ which coq.ocamlPackages.findlib ]
++ optional useDune2 coq.ocamlPackages.dune_2
++ optional (useDune2 || mlPlugin) coq.ocamlPackages.ocaml
++ optional useDune coq.ocamlPackages.dune_3
++ optional (useDune || mlPlugin) coq.ocamlPackages.ocaml
++ (args.nativeBuildInputs or []) ++ extraNativeBuildInputs);
buildInputs = args.overrideBuildInputs
or ([ coq ] ++ (args.buildInputs or []) ++ extraBuildInputs);
@ -107,7 +107,7 @@ stdenv.mkDerivation (removeAttrs ({
coqlib-flags ++ docdir-flags ++
extraInstallFlags;
})
// (optionalAttrs useDune2 {
// (optionalAttrs useDune {
buildPhase = ''
runHook preBuild
dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}

2
pkgs/development/coq-modules/addition-chains/default.nix
View File

@ -19,7 +19,7 @@ mkCoqDerivation {
propagatedBuildInputs = [ mathcomp-ssreflect mathcomp-algebra mathcomp-fingroup paramcoq ];
useDune2 = true;
useDune = true;
meta = {
description = "Exponentiation algorithms following addition chains";

2
pkgs/development/coq-modules/coqide/default.nix
View File

@ -22,7 +22,7 @@ with lib; mkCoqDerivation rec {
'';
prefixKey = "-prefix ";
useDune2 = true;
useDune = true;
buildInputs = [
copyDesktopItems

2
pkgs/development/coq-modules/gaia-hydras/default.nix
View File

@ -21,7 +21,7 @@ with lib; mkCoqDerivation rec {
mathcomp-zify
];
useDune2 = true;
useDune = true;
meta = {
description = "Comparison between ordinals in Gaia and Hydra battles";

2
pkgs/development/coq-modules/hydra-battles/default.nix
View File

@ -16,7 +16,7 @@ with lib;
{ case = range "8.11" "8.12"; out = "0.4"; }
] null;
useDune2 = true;
useDune = true;
meta = {
description = "Exploration of some properties of Kirby and Paris' hydra battles, with the help of Coq";

2
pkgs/development/coq-modules/mathcomp-word/default.nix
View File

@ -6,7 +6,7 @@ mkCoqDerivation {
pname = "word";
owner = "jasmin-lang";
repo = "coqword";
useDune2 = true;
useDune = true;
releaseRev = v: "v${v}";

6
pkgs/development/coq-modules/multinomials/default.nix
View File

@ -1,5 +1,5 @@
{ coq, mkCoqDerivation, mathcomp, mathcomp-finmap, mathcomp-bigenough,
lib, version ? null, useDune2 ? false }@args:
lib, version ? null, useDune ? false }@args:
with lib; mkCoqDerivation {
namePrefix = [ "coq" "mathcomp" ];
@ -31,7 +31,7 @@ with lib; mkCoqDerivation {
"1.0".sha256 = "1qmbxp1h81cy3imh627pznmng0kvv37k4hrwi2faa101s6bcx55m";
};
useDune2ifVersion = v: versions.isGe "1.5.3" v || v == "dev";
useDuneifVersion = v: versions.isGe "1.5.3" v || v == "dev";
preConfigure = ''
patchShebangs configure || true
@ -45,4 +45,4 @@ with lib; mkCoqDerivation {
license = licenses.cecill-c;
};
}
// optionalAttrs (args?useDune2) { inherit useDune2; }
// optionalAttrs (args?useDune) { inherit useDune; }

2
pkgs/development/coq-modules/serapi/default.nix
View File

@ -27,7 +27,7 @@ in
{ case = isEq "8.10"; out = "8.10.0+0.7.2"; }
] null;
useDune2 = true;
useDune = true;
patches = [ ./janestreet-0.15.patch ];

2
pkgs/development/coq-modules/topology/default.nix
View File

@ -25,7 +25,7 @@ mkCoqDerivation rec {
propagatedBuildInputs = [ zorns-lemma ];
useDune2ifVersion = versions.isGe "9.0";
useDuneifVersion = versions.isGe "9.0";
meta = {
description = "General topology in Coq";

2
pkgs/development/coq-modules/zorns-lemma/default.nix
View File

@ -25,7 +25,7 @@ with lib;
{ case = "8.5"; out = "8.5.0"; }
] null;
useDune2ifVersion = versions.isGe "9.0";
useDuneifVersion = versions.isGe "9.0";
meta = {
description = "Development of basic set theory";