Symmetric mkRocqDerivation / mkCoqDerivation (#537814)

This commit is contained in:
Théo Zimmermann 2026-07-06 11:29:34 +00:00 committed by GitHub
commit 5e0de9d493
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 8 additions and 28 deletions

View file

@ -41,7 +41,7 @@ in
pname, pname,
version ? null, version ? null,
fetcher ? null, fetcher ? null,
owner ? "coq-community", owner ? "rocq-community",
domain ? "github.com", domain ? "github.com",
repo ? pname, repo ? pname,
defaultVersion ? null, defaultVersion ? null,
@ -98,7 +98,6 @@ let
"dropAttrs" "dropAttrs"
"dropDerivationAttrs" "dropDerivationAttrs"
"keepAttrs" "keepAttrs"
"enableParallelBuilding"
] ]
++ dropAttrs ++ dropAttrs
) keepAttrs; ) keepAttrs;
@ -158,27 +157,11 @@ let
append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-"; append-version = p: n: p + display-pkg n "" coqPackages.${n}.version + "-";
prefix-name = foldl append-version "" namePrefix; prefix-name = foldl append-version "" namePrefix;
useDune = args.useDune or (useDuneifVersion fetched.version); useDune = args.useDune or (useDuneifVersion fetched.version);
coqlib-flags = coqlib-flags = [
switch coq.coq-version "COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
[ "COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
{ ];
case = v: versions.isLe "8.6" v && v != "dev"; docdir-flags = [ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
out = [ "COQLIB=$(out)/lib/coq/${coq.coq-version}/" ];
}
]
[
"COQLIBINSTALL=$(out)/lib/coq/${coq.coq-version}/user-contrib"
"COQPLUGININSTALL=$(OCAMLFIND_DESTDIR)"
];
docdir-flags =
switch coq.coq-version
[
{
case = v: versions.isLe "8.6" v && v != "dev";
out = [ "DOCDIR=$(out)/share/coq/${coq.coq-version}/" ];
}
]
[ "COQDOCINSTALL=$(out)/share/coq/${coq.coq-version}/user-contrib" ];
in in
stdenv.mkDerivation ( stdenv.mkDerivation (
@ -202,10 +185,7 @@ stdenv.mkDerivation (
); );
buildInputs = buildInputs =
args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs); args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs);
enableParallelBuilding = inherit enableParallelBuilding;
lib.warnIf (args ? enableParallelBuilding && args.enableParallelBuilding == true)
"mkCoqDerivation: enableParallelBuilding is enabled by default; remove the explicit setting"
enableParallelBuilding;
meta = meta =
( (

View file

@ -41,7 +41,7 @@ in
pname, pname,
version ? null, version ? null,
fetcher ? null, fetcher ? null,
owner ? "coq-community", owner ? "rocq-community",
domain ? "github.com", domain ? "github.com",
repo ? pname, repo ? pname,
defaultVersion ? null, defaultVersion ? null,