mkCoqDerivation: warn on superfluous enableParallelBuilding (#485720)

This commit is contained in:
Théo Zimmermann
2026-02-19 10:04:17 +00:00
committed by GitHub
3 changed files with 5 additions and 4 deletions
+5 -1
View File
@@ -98,6 +98,7 @@ let
"dropAttrs"
"dropDerivationAttrs"
"keepAttrs"
"enableParallelBuilding"
]
++ dropAttrs
) keepAttrs;
@@ -201,7 +202,10 @@ stdenv.mkDerivation (
);
buildInputs =
args.overrideBuildInputs or ([ coq ] ++ (args.buildInputs or [ ]) ++ extraBuildInputs);
inherit enableParallelBuilding;
enableParallelBuilding =
lib.warnIf (args ? enableParallelBuilding && args.enableParallelBuilding == true)
"mkCoqDerivation: enableParallelBuilding is enabled by default; remove the explicit setting"
enableParallelBuilding;
meta =
(
@@ -92,8 +92,6 @@ let
MenhirLib
];
enableParallelBuilding = true;
postPatch = ''
substituteInPlace ./configure \
--replace \$\{toolprefix\}ar 'ar' \
@@ -68,7 +68,6 @@ mkCoqDerivation rec {
++ lib.optionals (lib.versions.isGe "4.2.0" defaultVersion) [ gnuplot_qt ];
useMelquiondRemake.logpath = "Interval";
mlPlugin = true;
enableParallelBuilding = true;
meta = {
description = "Tactics for simplifying the proofs of inequalities on expressions of real numbers for the Coq proof assistant";