mirror of
https://github.com/NixOS/nixpkgs.git
synced 2024-09-29 07:32:58 +00:00
Merge pull request #299010 from philiptaron/issue-208242/coq-modules
coq-modules: avoid top-level `with ...;` expressions
This commit is contained in:
commit
c4bed1881c
@ -1,6 +1,6 @@
|
|||||||
{ lib, mkCoqDerivation, which, coq, version ? null }:
|
{ lib, mkCoqDerivation, which, coq, version ? null }:
|
||||||
|
|
||||||
with builtins; with lib; let
|
let
|
||||||
elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
|
elpi = coq.ocamlPackages.elpi.override (lib.switch coq.coq-version [
|
||||||
{ case = "8.11"; out = { version = "1.11.4"; };}
|
{ case = "8.11"; out = { version = "1.11.4"; };}
|
||||||
{ case = "8.12"; out = { version = "1.12.0"; };}
|
{ case = "8.12"; out = { version = "1.12.0"; };}
|
||||||
@ -71,7 +71,7 @@ in mkCoqDerivation {
|
|||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
description = "Coq plugin embedding ELPI";
|
description = "Coq plugin embedding ELPI";
|
||||||
maintainers = [ maintainers.cohencyril ];
|
maintainers = [ lib.maintainers.cohencyril ];
|
||||||
license = licenses.lgpl21Plus;
|
license = lib.licenses.lgpl21Plus;
|
||||||
};
|
};
|
||||||
}
|
}
|
||||||
|
@ -1,10 +1,10 @@
|
|||||||
{ lib,
|
{ lib,
|
||||||
mkCoqDerivation, recurseIntoAttrs,
|
mkCoqDerivation,
|
||||||
mathcomp, mathcomp-finmap, mathcomp-bigenough,
|
mathcomp, mathcomp-finmap, mathcomp-bigenough,
|
||||||
hierarchy-builder,
|
hierarchy-builder,
|
||||||
single ? false,
|
single ? false,
|
||||||
coqPackages, coq, version ? null }@args:
|
coqPackages, coq, version ? null }@args:
|
||||||
with builtins // lib;
|
|
||||||
let
|
let
|
||||||
repo = "analysis";
|
repo = "analysis";
|
||||||
owner = "math-comp";
|
owner = "math-comp";
|
||||||
@ -30,20 +30,21 @@ let
|
|||||||
release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
|
release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
|
||||||
release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
|
release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
|
||||||
|
|
||||||
defaultVersion = with versions; lib.switch [ coq.version mathcomp.version ] [
|
defaultVersion = let inherit (lib.versions) range; in
|
||||||
{ cases = [ (range "8.17" "8.19") (range "2.0.0" "2.2.0") ]; out = "1.1.0"; }
|
lib.switch [ coq.version mathcomp.version ] [
|
||||||
|
{ cases = [ (range "8.17" "8.19") (range "2.0.0" "2.2.0") ]; out = "1.1.0"; }
|
||||||
{ cases = [ (range "8.17" "8.19") (range "1.17.0" "1.19.0") ]; out = "0.7.0"; }
|
{ cases = [ (range "8.17" "8.19") (range "1.17.0" "1.19.0") ]; out = "0.7.0"; }
|
||||||
{ cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.7"; }
|
{ cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.7"; }
|
||||||
{ cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.6"; }
|
{ cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.6"; }
|
||||||
{ cases = [ (range "8.14" "8.18") (range "1.15.0" "1.17.0") ]; out = "0.6.5"; }
|
{ cases = [ (range "8.14" "8.18") (range "1.15.0" "1.17.0") ]; out = "0.6.5"; }
|
||||||
{ cases = [ (range "8.14" "8.18") (range "1.13.0" "1.16.0") ]; out = "0.6.1"; }
|
{ cases = [ (range "8.14" "8.18") (range "1.13.0" "1.16.0") ]; out = "0.6.1"; }
|
||||||
{ cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; }
|
{ cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; }
|
||||||
{ cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; }
|
{ cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; }
|
||||||
{ cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; }
|
{ cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; }
|
||||||
{ cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; }
|
{ cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; }
|
||||||
{ cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; }
|
{ cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; }
|
||||||
{ cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; }
|
{ cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; }
|
||||||
{ cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; }
|
{ cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; }
|
||||||
] null;
|
] null;
|
||||||
|
|
||||||
# list of analysis packages sorted by dependency order
|
# list of analysis packages sorted by dependency order
|
||||||
@ -52,7 +53,7 @@ let
|
|||||||
mathcomp_ = package: let
|
mathcomp_ = package: let
|
||||||
classical-deps = [ mathcomp.algebra mathcomp-finmap ];
|
classical-deps = [ mathcomp.algebra mathcomp-finmap ];
|
||||||
analysis-deps = [ mathcomp.field mathcomp-bigenough ];
|
analysis-deps = [ mathcomp.field mathcomp-bigenough ];
|
||||||
intra-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages)));
|
intra-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages)));
|
||||||
pkgpath = if package == "single" then "."
|
pkgpath = if package == "single" then "."
|
||||||
else if package == "analysis" then "theories" else "${package}";
|
else if package == "analysis" then "theories" else "${package}";
|
||||||
pname = if package == "single" then "mathcomp-analysis-single"
|
pname = if package == "single" then "mathcomp-analysis-single"
|
||||||
@ -64,8 +65,8 @@ let
|
|||||||
|
|
||||||
propagatedBuildInputs =
|
propagatedBuildInputs =
|
||||||
intra-deps
|
intra-deps
|
||||||
++ optionals (elem package [ "classical" "single" ]) classical-deps
|
++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps
|
||||||
++ optionals (elem package [ "analysis" "single" ]) analysis-deps;
|
++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps;
|
||||||
|
|
||||||
preBuild = ''
|
preBuild = ''
|
||||||
cd ${pkgpath}
|
cd ${pkgpath}
|
||||||
@ -73,26 +74,26 @@ let
|
|||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
description = "Analysis library compatible with Mathematical Components";
|
description = "Analysis library compatible with Mathematical Components";
|
||||||
maintainers = [ maintainers.cohencyril ];
|
maintainers = [ lib.maintainers.cohencyril ];
|
||||||
license = licenses.cecill-c;
|
license = lib.licenses.cecill-c;
|
||||||
};
|
};
|
||||||
|
|
||||||
passthru = genAttrs packages mathcomp_;
|
passthru = lib.genAttrs packages mathcomp_;
|
||||||
});
|
});
|
||||||
# split packages didn't exist before 0.6, so bulding nothing in that case
|
# split packages didn't exist before 0.6, so bulding nothing in that case
|
||||||
patched-derivation1 = derivation.overrideAttrs (o:
|
patched-derivation1 = derivation.overrideAttrs (o:
|
||||||
optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" &&
|
lib.optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" &&
|
||||||
o.version != null && o.version != "dev" && versions.isLt "0.6" o.version)
|
o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version)
|
||||||
{ preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; }
|
{ preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; }
|
||||||
);
|
);
|
||||||
patched-derivation2 = patched-derivation1.overrideAttrs (o:
|
patched-derivation2 = patched-derivation1.overrideAttrs (o:
|
||||||
optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" &&
|
lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" &&
|
||||||
o.version != null && o.version != "dev" && versions.isLt "0.6" o.version)
|
o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version)
|
||||||
{ preBuild = ""; }
|
{ preBuild = ""; }
|
||||||
);
|
);
|
||||||
patched-derivation = patched-derivation2.overrideAttrs (o:
|
patched-derivation = patched-derivation2.overrideAttrs (o:
|
||||||
optionalAttrs (o.version != null
|
lib.optionalAttrs (o.version != null
|
||||||
&& (o.version == "dev" || versions.isGe "0.3.4" o.version))
|
&& (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
|
||||||
{
|
{
|
||||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
|
propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
|
||||||
}
|
}
|
||||||
|
@ -11,14 +11,15 @@
|
|||||||
############################################################################
|
############################################################################
|
||||||
|
|
||||||
{ lib, ncurses, graphviz, lua, fetchzip,
|
{ lib, ncurses, graphviz, lua, fetchzip,
|
||||||
mkCoqDerivation, recurseIntoAttrs, withDoc ? false, single ? false,
|
mkCoqDerivation, withDoc ? false, single ? false,
|
||||||
coqPackages, coq, hierarchy-builder, version ? null }@args:
|
coqPackages, coq, hierarchy-builder, version ? null }@args:
|
||||||
with builtins // lib;
|
|
||||||
let
|
let
|
||||||
repo = "math-comp";
|
repo = "math-comp";
|
||||||
owner = "math-comp";
|
owner = "math-comp";
|
||||||
withDoc = single && (args.withDoc or false);
|
withDoc = single && (args.withDoc or false);
|
||||||
defaultVersion = with versions; lib.switch coq.coq-version [
|
defaultVersion = let inherit (lib.versions) range; in
|
||||||
|
lib.switch coq.coq-version [
|
||||||
{ case = range "8.19" "8.19"; out = "1.19.0"; }
|
{ case = range "8.19" "8.19"; out = "1.19.0"; }
|
||||||
{ case = range "8.17" "8.18"; out = "1.18.0"; }
|
{ case = range "8.17" "8.18"; out = "1.18.0"; }
|
||||||
{ case = range "8.15" "8.18"; out = "1.17.0"; }
|
{ case = range "8.15" "8.18"; out = "1.17.0"; }
|
||||||
@ -63,7 +64,7 @@ let
|
|||||||
packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
|
packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
|
||||||
|
|
||||||
mathcomp_ = package: let
|
mathcomp_ = package: let
|
||||||
mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (head (splitList (lib.pred.equal package) packages)));
|
mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages)));
|
||||||
pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
|
pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
|
||||||
pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
|
pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
|
||||||
pkgallMake = ''
|
pkgallMake = ''
|
||||||
@ -74,12 +75,12 @@ let
|
|||||||
derivation = mkCoqDerivation ({
|
derivation = mkCoqDerivation ({
|
||||||
inherit version pname defaultVersion release releaseRev repo owner;
|
inherit version pname defaultVersion release releaseRev repo owner;
|
||||||
|
|
||||||
mlPlugin = versions.isLe "8.6" coq.coq-version;
|
mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
|
||||||
nativeBuildInputs = optionals withDoc [ graphviz lua ];
|
nativeBuildInputs = lib.optionals withDoc [ graphviz lua ];
|
||||||
buildInputs = [ ncurses ];
|
buildInputs = [ ncurses ];
|
||||||
propagatedBuildInputs = mathcomp-deps;
|
propagatedBuildInputs = mathcomp-deps;
|
||||||
|
|
||||||
buildFlags = optional withDoc "doc";
|
buildFlags = lib.optional withDoc "doc";
|
||||||
|
|
||||||
preBuild = ''
|
preBuild = ''
|
||||||
if [[ -f etc/utils/ssrcoqdep ]]
|
if [[ -f etc/utils/ssrcoqdep ]]
|
||||||
@ -90,16 +91,16 @@ let
|
|||||||
fi
|
fi
|
||||||
'' + ''
|
'' + ''
|
||||||
cd ${pkgpath}
|
cd ${pkgpath}
|
||||||
'' + optionalString (package == "all") pkgallMake;
|
'' + lib.optionalString (package == "all") pkgallMake;
|
||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
homepage = "https://math-comp.github.io/";
|
homepage = "https://math-comp.github.io/";
|
||||||
license = licenses.cecill-b;
|
license = lib.licenses.cecill-b;
|
||||||
maintainers = with maintainers; [ vbgl jwiegley cohencyril ];
|
maintainers = with lib.maintainers; [ vbgl jwiegley cohencyril ];
|
||||||
};
|
};
|
||||||
} // optionalAttrs (package != "single")
|
} // lib.optionalAttrs (package != "single")
|
||||||
{ passthru = genAttrs packages mathcomp_; }
|
{ passthru = lib.genAttrs packages mathcomp_; }
|
||||||
// optionalAttrs withDoc {
|
// lib.optionalAttrs withDoc {
|
||||||
htmldoc_template =
|
htmldoc_template =
|
||||||
fetchzip {
|
fetchzip {
|
||||||
url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
|
url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
|
||||||
@ -111,7 +112,7 @@ let
|
|||||||
'';
|
'';
|
||||||
postInstall =
|
postInstall =
|
||||||
let tgt = "$out/share/coq/${coq.coq-version}/"; in
|
let tgt = "$out/share/coq/${coq.coq-version}/"; in
|
||||||
optionalString withDoc ''
|
lib.optionalString withDoc ''
|
||||||
mkdir -p ${tgt}
|
mkdir -p ${tgt}
|
||||||
cp -r htmldoc ${tgt}
|
cp -r htmldoc ${tgt}
|
||||||
cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
|
cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
|
||||||
@ -120,20 +121,20 @@ let
|
|||||||
extraInstallFlags = [ "-f Makefile.coq" ];
|
extraInstallFlags = [ "-f Makefile.coq" ];
|
||||||
});
|
});
|
||||||
patched-derivation1 = derivation.overrideAttrs (o:
|
patched-derivation1 = derivation.overrideAttrs (o:
|
||||||
optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
|
lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
|
||||||
o.version != null && o.version != "dev" && versions.isLt "1.7" o.version)
|
o.version != null && o.version != "dev" && lib.versions.isLt "1.7" o.version)
|
||||||
{ preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; }
|
{ preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; }
|
||||||
);
|
);
|
||||||
patched-derivation2 = patched-derivation1.overrideAttrs (o:
|
patched-derivation2 = patched-derivation1.overrideAttrs (o:
|
||||||
optionalAttrs (versions.isLe "8.7" coq.coq-version ||
|
lib.optionalAttrs (lib.versions.isLe "8.7" coq.coq-version ||
|
||||||
(o.version != "dev" && versions.isLe "1.7" o.version))
|
(o.version != "dev" && lib.versions.isLe "1.7" o.version))
|
||||||
{
|
{
|
||||||
installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
|
installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
|
||||||
}
|
}
|
||||||
);
|
);
|
||||||
patched-derivation = patched-derivation2.overrideAttrs (o:
|
patched-derivation = patched-derivation2.overrideAttrs (o:
|
||||||
optionalAttrs (o.version != null
|
lib.optionalAttrs (o.version != null
|
||||||
&& (o.version == "dev" || versions.isGe "2.0.0" o.version))
|
&& (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
|
||||||
{
|
{
|
||||||
propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
|
propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
|
||||||
}
|
}
|
||||||
|
@ -1,11 +1,11 @@
|
|||||||
{ lib, fetchzip,
|
{ lib, fetchzip,
|
||||||
mkCoqDerivation, recurseIntoAttrs, single ? false,
|
mkCoqDerivation, single ? false,
|
||||||
coqPackages, coq, equations, version ? null }@args:
|
coqPackages, coq, equations, version ? null }@args:
|
||||||
with builtins // lib;
|
|
||||||
let
|
let
|
||||||
repo = "metacoq";
|
repo = "metacoq";
|
||||||
owner = "MetaCoq";
|
owner = "MetaCoq";
|
||||||
defaultVersion = with versions; switch coq.coq-version [
|
defaultVersion = lib.switch coq.coq-version [
|
||||||
{ case = "8.11"; out = "1.0-beta2-8.11"; }
|
{ case = "8.11"; out = "1.0-beta2-8.11"; }
|
||||||
{ case = "8.12"; out = "1.0-beta2-8.12"; }
|
{ case = "8.12"; out = "1.0-beta2-8.12"; }
|
||||||
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
|
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
|
||||||
@ -36,14 +36,14 @@ let
|
|||||||
releaseRev = v: "v${v}";
|
releaseRev = v: "v${v}";
|
||||||
|
|
||||||
# list of core metacoq packages sorted by dependency order
|
# list of core metacoq packages sorted by dependency order
|
||||||
packages = if versionAtLeast coq.coq-version "8.17"
|
packages = if lib.versionAtLeast coq.coq-version "8.17"
|
||||||
then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]
|
then [ "utils" "common" "template-coq" "pcuic" "safechecker" "template-pcuic" "erasure" "quotation" "safechecker-plugin" "erasure-plugin" "all" ]
|
||||||
else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
|
else [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
|
||||||
|
|
||||||
template-coq = metacoq_ "template-coq";
|
template-coq = metacoq_ "template-coq";
|
||||||
|
|
||||||
metacoq_ = package: let
|
metacoq_ = package: let
|
||||||
metacoq-deps = lib.optionals (package != "single") (map metacoq_ (head (splitList (lib.pred.equal package) packages)));
|
metacoq-deps = lib.optionals (package != "single") (map metacoq_ (lib.head (lib.splitList (lib.pred.equal package) packages)));
|
||||||
pkgpath = if package == "single" then "./" else "./${package}";
|
pkgpath = if package == "single" then "./" else "./${package}";
|
||||||
pname = if package == "all" then "metacoq" else "metacoq-${package}";
|
pname = if package == "all" then "metacoq" else "metacoq-${package}";
|
||||||
pkgallMake = ''
|
pkgallMake = ''
|
||||||
@ -57,7 +57,7 @@ let
|
|||||||
mlPlugin = true;
|
mlPlugin = true;
|
||||||
propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
|
propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
|
||||||
|
|
||||||
patchPhase = if versionAtLeast coq.coq-version "8.17" then ''
|
patchPhase = if lib.versionAtLeast coq.coq-version "8.17" then ''
|
||||||
patchShebangs ./configure.sh
|
patchShebangs ./configure.sh
|
||||||
patchShebangs ./template-coq/update_plugin.sh
|
patchShebangs ./template-coq/update_plugin.sh
|
||||||
patchShebangs ./template-coq/gen-src/to-lower.sh
|
patchShebangs ./template-coq/gen-src/to-lower.sh
|
||||||
@ -76,11 +76,11 @@ let
|
|||||||
sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh
|
sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./pcuic/clean_extraction.sh ./safechecker/clean_extraction.sh ./erasure/clean_extraction.sh
|
||||||
'' ;
|
'' ;
|
||||||
|
|
||||||
configurePhase = optionalString (package == "all") pkgallMake + ''
|
configurePhase = lib.optionalString (package == "all") pkgallMake + ''
|
||||||
touch ${pkgpath}/metacoq-config
|
touch ${pkgpath}/metacoq-config
|
||||||
'' + optionalString (elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) ''
|
'' + lib.optionalString (lib.elem package ["safechecker" "erasure" "template-pcuic" "quotation" "safechecker-plugin" "erasure-plugin"]) ''
|
||||||
echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
|
echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
|
||||||
'' + optionalString (package == "single") ''
|
'' + lib.optionalString (package == "single") ''
|
||||||
./configure.sh local
|
./configure.sh local
|
||||||
'';
|
'';
|
||||||
|
|
||||||
@ -90,17 +90,17 @@ let
|
|||||||
|
|
||||||
meta = {
|
meta = {
|
||||||
homepage = "https://metacoq.github.io/";
|
homepage = "https://metacoq.github.io/";
|
||||||
license = licenses.mit;
|
license = lib.licenses.mit;
|
||||||
maintainers = with maintainers; [ cohencyril ];
|
maintainers = with lib.maintainers; [ cohencyril ];
|
||||||
};
|
};
|
||||||
} // optionalAttrs (package != "single")
|
} // lib.optionalAttrs (package != "single")
|
||||||
{ passthru = genAttrs packages metacoq_; })
|
{ passthru = lib.genAttrs packages metacoq_; })
|
||||||
).overrideAttrs (o:
|
).overrideAttrs (o:
|
||||||
let requiresOcamlStdlibShims = versionAtLeast o.version "1.0-8.16" ||
|
let requiresOcamlStdlibShims = lib.versionAtLeast o.version "1.0-8.16" ||
|
||||||
(o.version == "dev" && (versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;
|
(o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev")) ;
|
||||||
in
|
in
|
||||||
{
|
{
|
||||||
propagatedBuildInputs = o.propagatedBuildInputs ++ optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
|
propagatedBuildInputs = o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
|
||||||
});
|
});
|
||||||
in derivation;
|
in derivation;
|
||||||
in
|
in
|
||||||
|
Loading…
Reference in New Issue
Block a user