mirror of
https://github.com/NixOS/nixpkgs.git
synced 2024-12-23 14:13:35 +00:00
d113661156
- put `findlib` in `buildInputs` of `mkCoqDerivation` to make sure `coq` packages find their ocaml plugin dependencies, - use `propagatedBuildInputs` to make sure ocaml plugin dependencies are in path, - updated `coqPackage.heq` (broken url), - fixed use of `DESTDIR` and `COQMF_COQLIB` in mkCoqDerivation, - adding `COQCORELIB` environement variable to put ocaml plugin files in the right place, - make `metaFetch` available from `coqPackages`
75 lines
3.0 KiB
Nix
75 lines
3.0 KiB
Nix
{ lib, fetchzip,
|
|
mkCoqDerivation, recurseIntoAttrs, single ? false,
|
|
coqPackages, coq, equations, version ? null }@args:
|
|
with builtins // lib;
|
|
let
|
|
repo = "metacoq";
|
|
owner = "MetaCoq";
|
|
defaultVersion = with versions; switch coq.coq-version [
|
|
{ case = "8.11"; out = "1.0-beta2-8.11"; }
|
|
{ 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)
|
|
# { case = "8.13"; out = "1.0-beta2-8.13"; }
|
|
] null;
|
|
release = {
|
|
"1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
|
|
"1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
|
|
"1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8=";
|
|
};
|
|
releaseRev = v: "v${v}";
|
|
|
|
# list of core metacoq packages sorted by dependency order
|
|
packages = [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
|
|
|
|
template-coq = metacoq_ "template-coq";
|
|
|
|
metacoq_ = package: let
|
|
metacoq-deps = if package == "single" then []
|
|
else map metacoq_ (head (splitList (pred.equal package) packages));
|
|
pkgpath = if package == "single" then "./" else "./${package}";
|
|
pname = if package == "all" then "metacoq" else "metacoq-${package}";
|
|
pkgallMake = ''
|
|
mkdir all
|
|
echo "all:" > all/Makefile
|
|
echo "install:" >> all/Makefile
|
|
'' ;
|
|
derivation = mkCoqDerivation ({
|
|
inherit version pname defaultVersion release releaseRev repo owner;
|
|
|
|
mlPlugin = true;
|
|
propagatedBuildInputs = [ equations coq.ocamlPackages.zarith ] ++ metacoq-deps;
|
|
|
|
patchPhase = ''
|
|
patchShebangs ./configure.sh
|
|
patchShebangs ./template-coq/update_plugin.sh
|
|
patchShebangs ./template-coq/gen-src/to-lower.sh
|
|
patchShebangs ./pcuic/clean_extraction.sh
|
|
patchShebangs ./safechecker/clean_extraction.sh
|
|
patchShebangs ./erasure/clean_extraction.sh
|
|
echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
|
|
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 + ''
|
|
touch ${pkgpath}/metacoq-config
|
|
'' + optionalString (elem package ["safechecker" "erasure"]) ''
|
|
echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
|
|
'' + optionalString (package == "single") ''
|
|
./configure.sh local
|
|
'';
|
|
|
|
preBuild = ''
|
|
cd ${pkgpath}
|
|
'' ;
|
|
|
|
meta = {
|
|
homepage = "https://metacoq.github.io/";
|
|
license = licenses.mit;
|
|
maintainers = with maintainers; [ cohencyril ];
|
|
};
|
|
} // optionalAttrs (package != "single")
|
|
{ passthru = genAttrs packages metacoq_; });
|
|
in derivation;
|
|
in
|
|
metacoq_ (if single then "single" else "all")
|