pyrox.dev
coqPackages.metacoq: create package (#162639)
authored by Kenji Maillard and committed by GitHub 86a69080 defbaa09
+76
pkgs/development/coq-modules/metacoq/default.nix
+76
pkgs/development/coq-modules/metacoq/default.nix
···
1
+
{ lib, which, fetchzip,
2
+
mkCoqDerivation, recurseIntoAttrs, single ? false,
3
+
coqPackages, coq, equations, version ? null }@args:
4
+
with builtins // lib;
5
+
let
6
+
repo = "metacoq";
7
+
owner = "MetaCoq";
8
+
defaultVersion = with versions; switch coq.coq-version [
9
+
{ case = "8.11"; out = "1.0-beta2-8.11"; }
10
+
{ case = "8.12"; out = "1.0-beta2-8.12"; }
11
+
# Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
12
+
# { case = "8.13"; out = "1.0-beta2-8.13"; }
13
+
] null;
14
+
release = {
15
+
"1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
16
+
"1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
17
+
"1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8=";
18
+
};
19
+
releaseRev = v: "v${v}";
20
+
21
+
# list of core metacoq packages sorted by dependency order
22
+
packages = [ "template-coq" "pcuic" "safechecker" "erasure" "all" ];
23
+
24
+
template-coq = metacoq_ "template-coq";
25
+
26
+
metacoq_ = package: let
27
+
metacoq-deps = if package == "single" then []
28
+
else map metacoq_ (head (splitList (pred.equal package) packages));
29
+
pkgpath = if package == "single" then "./" else "./${package}";
30
+
pname = if package == "all" then "metacoq" else "metacoq-${package}";
31
+
pkgallMake = ''
32
+
mkdir all
33
+
echo "all:" > all/Makefile
34
+
echo "install:" >> all/Makefile
35
+
'' ;
36
+
derivation = mkCoqDerivation ({
37
+
inherit version pname defaultVersion release releaseRev repo owner;
38
+
39
+
extraNativeBuildInputs = [ which ];
40
+
mlPlugin = true;
41
+
extraBuildInputs = [ coq.ocamlPackages.zarith ];
42
+
propagatedBuildInputs = [ equations ] ++ metacoq-deps;
43
+
44
+
patchPhase = ''
45
+
patchShebangs ./configure.sh
46
+
patchShebangs ./template-coq/update_plugin.sh
47
+
patchShebangs ./template-coq/gen-src/to-lower.sh
48
+
patchShebangs ./pcuic/clean_extraction.sh
49
+
patchShebangs ./safechecker/clean_extraction.sh
50
+
patchShebangs ./erasure/clean_extraction.sh
51
+
echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
52
+
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
53
+
'' ;
54
+
55
+
configurePhase = optionalString (package == "all") pkgallMake + ''
56
+
touch ${pkgpath}/metacoq-config
57
+
'' + optionalString (elem package ["safechecker" "erasure"]) ''
58
+
echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
59
+
'' + optionalString (package == "single") ''
60
+
./configure.sh local
61
+
'';
62
+
63
+
preBuild = ''
64
+
cd ${pkgpath}
65
+
'' ;
66
+
67
+
meta = {
68
+
homepage = "https://metacoq.github.io/";
69
+
license = licenses.mit;
70
+
maintainers = with maintainers; [ cohencyril ];
71
+
};
72
+
} // optionalAttrs (package != "single")
73
+
{ passthru = genAttrs packages metacoq_; });
74
+
in derivation;
75
+
in
76
+
metacoq_ (if single then "single" else "all")
+1
pkgs/top-level/coq-packages.nix
+1
pkgs/top-level/coq-packages.nix
···
77
77
mathcomp-word = callPackage ../development/coq-modules/mathcomp-word {};
78
78
mathcomp-zify = callPackage ../development/coq-modules/mathcomp-zify {};
79
79
mathcomp-tarjan = callPackage ../development/coq-modules/mathcomp-tarjan {};
80
+
metacoq = callPackage ../development/coq-modules/metacoq { };
80
81
metalib = callPackage ../development/coq-modules/metalib { };
81
82
multinomials = callPackage ../development/coq-modules/multinomials {};
82
83
odd-order = callPackage ../development/coq-modules/odd-order { };