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

Delete duplicated code and make mkCoqDerivation a wrapper on top of mkRocqDerivation (#537856)

Browse Source
This commit is contained in:
Vincent Laporte
2026-07-13 07:41:58 +00:00
committed by GitHub
parent 6ae84c662d 962d8fb3ed
commit 17be5c5fe7
11 changed files with 40 additions and 263 deletions
Download Patch File Download Diff File Expand all files Collapse all files
doc/languages-frameworks/rocq.section.md
+2
View File
@@ -74,6 +74,8 @@ The recommended way of defining a derivation for a Rocq library, is to use the `
* `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 `COQLIBINSTALL` and `COQPLUGININSTALL` so as to install in the proper subdirectory. Indeed Rocq libraries should be installed in `$(out)/lib/coq/${rocq-core.rocq-version}/user-contrib/`. Such directories are automatically added to the `$ROCQPATH` environment variable by the hook defined in the Rocq derivation.
* `setROCQBIN` (optional, defaults to `true`), by default, the environment variable `$ROCQBIN` is set to the current Rocq's binary, but one can disable this behavior by setting it to `false`,
* `useCoq` (optional, defaults to `false`), adds the Coq compatibility binaries to the build environment, which is necessary for some packages that still depend on them and sets `COQBIN` to the path of the `coqc` binary (if `setROCQBIN` is also set to `true`). A wrapper `mkCoqDerivation` is provided that sets this option to `true`.
* `useCoqifVersion` (optional, defaults to `(x: false)`), adds the Coq compatibility binaries to the build environment if the provided predicate evaluates to true on the version. This can be useful for supporting old package versions that need the Coq compatibility binaries, while newer versions do not.
* `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`.
pkgs/applications/science/logic/coq/default.nix
+1 -1
View File
@@ -79,7 +79,7 @@ let
};
releaseRev = v: "V${v}";
fetched =
import ../../../../build-support/coq/meta-fetch/default.nix
import ../../../../build-support/rocq/meta-fetch/default.nix
{
inherit
lib
pkgs/applications/science/logic/rocq-core/default.nix
+1 -1
View File
@@ -32,7 +32,7 @@ let
};
releaseRev = v: "V${v}";
fetched =
import ../../../../build-support/coq/meta-fetch/default.nix
import ../../../../build-support/rocq/meta-fetch/default.nix
{
inherit
lib
pkgs/build-support/coq/default.nix
-246
View File
@@ -1,246 +0,0 @@
{
lib,
stdenv,
coqPackages,
coq,
which,
fetchzip,
fetchurl,
dune,
}@args:
let
lib = import ./extra-lib.nix {
inherit (args) lib;
};
inherit (lib)
concatStringsSep
flip
foldl
isFunction
isString
optional
optionalAttrs
optionals
optionalString
pred
remove
switch
versions
;
inherit (lib.attrsets) removeAttrs;
inherit (lib.strings) match;
isGitHubDomain = d: match "^github.*" d != null;
isGitLabDomain = d: match "^gitlab.*" d != null;
in
{
pname,
version ? null,
fetcher ? null,
owner ? "rocq-community",
domain ? "github.com",
repo ? pname,
defaultVersion ? null,
releaseRev ? (v: v),
displayVersion ? { },
release ? { },
buildInputs ? [ ],
nativeBuildInputs ? [ ],
extraBuildInputs ? [ ],
extraNativeBuildInputs ? [ ],
overrideBuildInputs ? [ ],
overrideNativeBuildInputs ? [ ],
namePrefix ? [ "coq" ],
enableParallelBuilding ? true,
extraInstallFlags ? [ ],
setCOQBIN ? true,
mlPlugin ? false,
useMelquiondRemake ? null,
dropAttrs ? [ ],
keepAttrs ? [ ],
dropDerivationAttrs ? [ ],
useDuneifVersion ? (x: false),
useDune ? false,
opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
...
}@args:
let
args-to-remove = foldl (flip remove) (
[
"version"
"fetcher"
"repo"
"owner"
"domain"
"releaseRev"
"displayVersion"
"defaultVersion"
"useMelquiondRemake"
"release"
"buildInputs"
"nativeBuildInputs"
"extraBuildInputs"
"extraNativeBuildInputs"
"overrideBuildInputs"
"overrideNativeBuildInputs"
"namePrefix"
"meta"
"useDuneifVersion"
"useDune"
"opam-name"
"extraInstallFlags"
"setCOQBIN"
"mlPlugin"
"dropAttrs"
"dropDerivationAttrs"
"keepAttrs"
"env"
]
++ dropAttrs
) keepAttrs;
fetch =
import ../coq/meta-fetch/default.nix
{
inherit
lib
stdenv
fetchzip
fetchurl
;
}
(
{
inherit release releaseRev;
location = { inherit domain owner repo; };
}
// optionalAttrs (args ? fetcher) { inherit fetcher; }
);
fetched = fetch (if version != null then version else defaultVersion);
display-pkg =
n: sep: v:
let
d = displayVersion.${n} or (if sep == "" then ".." else true);
in
n
+ optionalString (v != "" && v != null) (
switch d [
{
case = true;
out = sep + v;
}
{
case = ".";
out = sep + versions.major v;
}
{
case = "..";
out = sep + versions.majorMinor v;
}
{
case = "...";
out = sep + versions.majorMinorPatch v;
}
{
case = isFunction;
out = optionalString (d v != "") (sep + d v);
}
{
case = isString;
out = optionalString (d != "") (sep + d);
}
] ""
)
+ optionalString (v == null) "-broken";
append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
prefix-name = foldl append-version "" namePrefix;
useDune = args.useDune or (useDuneifVersion fetched.version);
coqlib-flags = [
"COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
"COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
];
docdir-flags = [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
COQUSERCONTRIB = "$out/lib/coq/${coq.coq-version}/user-contrib";
in
stdenv.mkDerivation (
removeAttrs (
{
name = prefix-name + (display-pkg pname "-" fetched.version);
inherit (fetched) version src;
nativeBuildInputs =
args.overrideNativeBuildInputs or (
[ which ]
++ optional useDune dune
++ optionals (useDune || mlPlugin) [
coq.ocamlPackages.ocaml
coq.ocamlPackages.findlib
]
++ (args.nativeBuildInputs or [ ])
++ extraNativeBuildInputs
);
buildInputs =
args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs);
inherit enableParallelBuilding;
env =
optionalAttrs setCOQBIN {
COQBIN = "${coq}/bin/";
}
// optionalAttrs (args ? useMelquiondRemake) {
inherit COQUSERCONTRIB;
}
// (args.env or { });
meta =
(
{
platforms = coq.meta.platforms;
}
// (switch domain [
{
case = pred.union isGitHubDomain isGitLabDomain;
out = {
homepage = "https://${domain}/${owner}/${repo}";
};
}
] { })
// optionalAttrs (fetched.broken or false) {
coqFilter = true;
broken = true;
}
)
// (args.meta or { });
}
// (optionalAttrs (!args ? installPhase && !args ? useMelquiondRemake) {
installFlags = coqlib-flags ++ docdir-flags ++ extraInstallFlags;
})
// (optionalAttrs useDune {
buildPhase = ''
runHook preBuild
dune build -p ${opam-name} ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
runHook postBuild
'';
installPhase = ''
runHook preInstall
dune install --prefix=$out --libdir $OCAMLFIND_DESTDIR ${opam-name}
mkdir $out/lib/coq/
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
runHook postInstall
'';
})
// (optionalAttrs (args ? useMelquiondRemake) {
preConfigurePhases = [ "autoconf" ];
configureFlags = [ "--libdir=${COQUSERCONTRIB}/${useMelquiondRemake.logpath or ""}" ];
buildPhase = "./remake -j$NIX_BUILD_CORES";
installPhase = "./remake install";
})
// (removeAttrs args args-to-remove)
) dropDerivationAttrs
)
pkgs/build-support/rocq/default.nix
+12 -4
View File
@@ -3,15 +3,16 @@
stdenv,
rocqPackages,
rocq-core,
coq,
which,
fetchzip,
fetchurl,
dune,
}@args:
}@args0:
let
lib = import ./extra-lib.nix {
inherit (args) lib;
inherit (args0) lib;
};
inherit (lib)
@@ -66,6 +67,8 @@ in
useDuneifVersion ? (x: false),
useDune ? false,
opam-name ? (concatStringsSep "-" (namePrefix ++ [ pname ])),
useCoq ? false,
useCoqifVersion ? (x: false),
...
}@args:
let
@@ -99,11 +102,13 @@ let
"dropDerivationAttrs"
"keepAttrs"
"env"
"useCoq"
"useCoqifVersion"
]
++ dropAttrs
) keepAttrs;
fetch =
import ../coq/meta-fetch/default.nix
import ../rocq/meta-fetch/default.nix
{
inherit
lib
@@ -158,6 +163,8 @@ let
append-version = p: n: p + display-pkg n "" rocqPackages.${n}.version + "-";
prefix-name = foldl append-version "" namePrefix;
useDune = args.useDune or (useDuneifVersion fetched.version);
useCoq = args.useCoq or (useCoqifVersion fetched.version);
rocq-core = if useCoq then coq // { rocq-version = coq.coq-version; } else args0.rocq-core;
rocqlib-flags = [
"COQLIBINSTALL=$(out)/lib/coq/${rocq-core.rocq-version}/user-contrib"
"COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
@@ -190,9 +197,10 @@ stdenv.mkDerivation (
inherit enableParallelBuilding;
env =
optionalAttrs setROCQBIN {
optionalAttrs (setROCQBIN && !useCoq) {
ROCQBIN = "${rocq-core}/bin/";
}
// optionalAttrs (setROCQBIN && useCoq) { COQBIN = "${rocq-core}/bin/"; }
// optionalAttrs (args ? useMelquiondRemake) {
inherit COQUSERCONTRIB;
}
pkgs/build-support/coq/meta-fetch/default.nix → pkgs/build-support/rocq/meta-fetch/default.nix
View File
pkgs/development/coq-modules/coq-elpi/default.nix
+4 -2
View File
@@ -1,6 +1,6 @@
{
lib,
mkCoqDerivation,
mkRocqDerivation,
which,
dune,
coq,
@@ -34,7 +34,9 @@ let
propagatedBuildInputs_wo_elpi = [
coq.ocamlPackages.findlib
];
derivation = mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
derivation = mkRocqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
useCoq = true;
namePrefix = [ "coq" ];
pname = "elpi";
repo = "coq-elpi";
owner = "LPCIC";
pkgs/development/coq-modules/stalmarck/default.nix
+4 -2
View File
@@ -1,6 +1,6 @@
{
lib,
mkCoqDerivation,
mkRocqDerivation,
dune,
coq,
stdlib,
@@ -39,7 +39,9 @@ let
else
"A two-level approach to prove tautologies using Stålmarck's algorithm in Coq.";
in
mkCoqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
mkRocqDerivation.override { dune = dune.override { version = "3.21.1"; }; } {
useCoq = true;
namePrefix = [ "coq" ];
inherit
version
pname
pkgs/development/coq-modules/vscoq-language-server/default.nix
+1 -1
View File
@@ -82,7 +82,7 @@ ocamlPackages.buildDunePackage {
license = lib.licenses.mit;
}
// lib.optionalAttrs (fetched.broken or false) {
coqFilter = true;
rocqFilter = true;
broken = true;
};
}
pkgs/top-level/coq-packages.nix
+14 -5
View File
@@ -27,14 +27,14 @@ let
self: coq:
let
callPackage = self.callPackage;
coqPackages = self // {
rocqPackages = self // {
recurseForDerivations = false;
};
in
{
inherit coqPackages lib;
inherit rocqPackages lib;
metaFetch = import ../build-support/coq/meta-fetch/default.nix {
metaFetch = import ../build-support/rocq/meta-fetch/default.nix {
inherit
lib
stdenv
@@ -42,7 +42,16 @@ let
fetchurl
;
};
mkCoqDerivation = lib.makeOverridable (callPackage ../build-support/coq { });
mkRocqDerivation = lib.makeOverridable (callPackage ../build-support/rocq { });
mkCoqDerivation =
args:
self.mkRocqDerivation (
{
useCoq = true;
namePrefix = [ "coq" ];
}
// args
);
coq = coq.overrideAttrs (oldAttrs: {
passthru = (oldAttrs.passthru or { }) // {
@@ -286,7 +295,7 @@ let
let
v = set.${name} or null;
in
lib.optional (!v.meta.coqFilter or false) (
lib.optional (!v.meta.rocqFilter or false) (
lib.nameValuePair name (
if lib.isAttrs v && v.recurseForDerivations or false then filterCoqPackages v else v
)
pkgs/top-level/rocq-packages.nix
+1 -1
View File
@@ -26,7 +26,7 @@ let
recurseForDerivations = false;
};
metaFetch = import ../build-support/coq/meta-fetch/default.nix {
metaFetch = import ../build-support/rocq/meta-fetch/default.nix {
inherit
lib
stdenv