tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 single ? false,
5 coq,
6 equations,
7 version ? null,
8}@args:
9
10let
11 repo = "metacoq";
12 owner = "MetaCoq";
13 defaultVersion =
14 let
15 case = case: out: { inherit case out; };
16 in
17 lib.switch coq.coq-version [
18 (case "8.11" "1.0-beta2-8.11")
19 (case "8.12" "1.0-beta2-8.12")
20 # Do not provide 8.13 because it does not compile with equations 1.3 provided by default (only 1.2.3)
21 # (case "8.13" "1.0-beta2-8.13")
22 (case "8.14" "1.1-8.14")
23 (case "8.15" "1.1-8.15")
24 (case "8.16" "1.1-8.16")
25 (case "8.17" "1.3.1-8.17")
26 (case "8.18" "1.3.1-8.18")
27 (case "8.19" "1.3.3-8.19")
28 (case "8.20" "1.3.4-8.20")
29 ] null;
30 release = {
31 "1.0-beta2-8.11".sha256 = "sha256-I9YNk5Di6Udvq5/xpLSNflfjRyRH8fMnRzbo3uhpXNs=";
32 "1.0-beta2-8.12".sha256 = "sha256-I8gpmU9rUQJh0qfp5KOgDNscVvCybm5zX4TINxO1TVA=";
33 "1.0-beta2-8.13".sha256 = "sha256-IC56/lEDaAylUbMCfG/3cqOBZniEQk8jmI053DBO5l8=";
34 "1.0-8.14".sha256 = "sha256-iRnaNeHt22JqxMNxOGPPycrO9EoCVjusR2s0GfON1y0=";
35 "1.0-8.15".sha256 = "sha256-8RUC5dHNfLJtJh+IZG4nPTAVC8ZKVh2BHedkzjwLf/k=";
36 "1.0-8.16".sha256 = "sha256-7rkCAN4PNnMgsgUiiLe2TnAliknN75s2SfjzyKCib/o=";
37 "1.1-8.14".sha256 = "sha256-6vViCNQl6BnGgOHX3P/OLfFXN4aUfv4RbDokfz2BgQI=";
38 "1.1-8.15".sha256 = "sha256-qCD3wFW4E+8vSVk4XoZ0EU4PVya0al+JorzS9nzmR/0=";
39 "1.1-8.16".sha256 = "sha256-cTK4ptxpPPlqxAhasZFX3RpSlsoTZwhTqs2A3BZy9sA=";
40 "1.2.1-8.17".sha256 = "sha256-FP4upuRsG8B5Q5FIr76t+ecRirrOUX0D1QiLq0/zMyE=";
41 "1.2.1-8.18".sha256 = "sha256-49g5db2Bv8HpltptJdxA7zrmgNFGC6arx5h2mKHhrko=";
42 "1.3.1-8.17".sha256 = "sha256-l0/QLC7V3zSk/FsaE2eL6tXy2BzbcI5MAk/c+FESwnc=";
43 "1.3.1-8.18".sha256 = "sha256-L6Ym4Auwqaxv5tRmJLSVC812dxCqdUU5aN8+t5HVYzY=";
44 "1.3.1-8.19".sha256 = "sha256-fZED/Uel1jt5XF83dR6HfyhSkfBdLkET8C/ArDgsm64=";
45 "1.3.2-8.19".sha256 = "sha256-e5Pm1AhaQrO6JoZylSXYWmeXY033QflQuCBZhxGH8MA=";
46 "1.3.2-8.20".sha256 = "sha256-4J7Ly4Fc2E/I6YqvzTLntVVls5t94OUOjVMKJyyJdw8=";
47 "1.3.3-8.19".sha256 = "sha256-SBTv49zQXZ+oGvIqWM53hjBKru9prFgZRv8gVgls40k=";
48 "1.3.4-8.20".sha256 = "sha256-ofRP0Uo48G2LBuIy/5ZLyK+iVZXleKiwfMEBD0rX9fQ=";
49 "1.3.4-9.0".sha256 = "sha256-BiAeuwL6WvDNs+ZGzPWj59kTS69J4kjrS3XIZyzpLOQ=";
50 };
51 releaseRev = v: "v${v}";
52
53 # list of core metacoq packages and their dependencies
54 packages = {
55 "utils" = [ ];
56 "common" = [ "utils" ];
57 "template-coq" = [ "common" ];
58 "pcuic" =
59 if (lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev") then
60 [ "common" ]
61 else
62 [ "template-coq" ];
63 "safechecker" = [ "pcuic" ];
64 "template-pcuic" = [
65 "template-coq"
66 "pcuic"
67 ];
68 "erasure" = [
69 "safechecker"
70 "template-pcuic"
71 ];
72 "quotation" = [
73 "template-coq"
74 "pcuic"
75 "template-pcuic"
76 ];
77 "safechecker-plugin" = [
78 "template-pcuic"
79 "safechecker"
80 ];
81 "erasure-plugin" = [
82 "template-pcuic"
83 "erasure"
84 ];
85 "translations" = [ "template-coq" ];
86 "all" = [
87 "safechecker-plugin"
88 "erasure-plugin"
89 "translations"
90 "quotation"
91 ];
92 };
93
94 template-coq = metacoq_ "template-coq";
95
96 metacoq_ =
97 package:
98 let
99 metacoq-deps = lib.optionals (package != "single") (map metacoq_ packages.${package});
100 pkgpath = if package == "single" then "./" else "./${package}";
101 pname = if package == "all" then "metacoq" else "metacoq-${package}";
102 pkgallMake = ''
103 mkdir all
104 echo "all:" > all/Makefile
105 echo "install:" >> all/Makefile
106 '';
107 derivation =
108 (mkCoqDerivation (
109 {
110 inherit
111 version
112 pname
113 defaultVersion
114 release
115 releaseRev
116 repo
117 owner
118 ;
119
120 mlPlugin = true;
121 propagatedBuildInputs = [
122 equations
123 coq.ocamlPackages.zarith
124 ]
125 ++ metacoq-deps;
126
127 patchPhase =
128 if lib.versionAtLeast coq.coq-version "8.17" || coq.coq-version == "dev" then
129 ''
130 patchShebangs ./configure.sh
131 patchShebangs ./template-coq/update_plugin.sh
132 patchShebangs ./template-coq/gen-src/to-lower.sh
133 patchShebangs ./safechecker-plugin/clean_extraction.sh
134 patchShebangs ./erasure-plugin/clean_extraction.sh
135 echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
136 sed -i -e 's/mv $i $newi;/mv $i tmp; mv tmp $newi;/' ./template-coq/gen-src/to-lower.sh ./safechecker-plugin/clean_extraction.sh ./erasure-plugin/clean_extraction.sh
137 ''
138 else
139 ''
140 patchShebangs ./configure.sh
141 patchShebangs ./template-coq/update_plugin.sh
142 patchShebangs ./template-coq/gen-src/to-lower.sh
143 patchShebangs ./pcuic/clean_extraction.sh
144 patchShebangs ./safechecker/clean_extraction.sh
145 patchShebangs ./erasure/clean_extraction.sh
146 echo "CAMLFLAGS+=-w -60 # Unused module" >> ./safechecker/Makefile.plugin.local
147 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
148 '';
149
150 configurePhase =
151 lib.optionalString (package == "all") pkgallMake
152 + ''
153 touch ${pkgpath}/metacoq-config
154 ''
155 +
156 lib.optionalString
157 (lib.elem package [
158 "erasure"
159 "template-pcuic"
160 "quotation"
161 "safechecker-plugin"
162 "erasure-plugin"
163 "translations"
164 ])
165 ''
166 echo "-I ${template-coq}/lib/coq/${coq.coq-version}/user-contrib/MetaCoq/Template/" > ${pkgpath}/metacoq-config
167 ''
168 + lib.optionalString (package == "single") ''
169 ./configure.sh local
170 '';
171
172 preBuild = ''
173 cd ${pkgpath}
174 '';
175
176 meta = {
177 homepage = "https://metacoq.github.io/";
178 license = lib.licenses.mit;
179 maintainers = with lib.maintainers; [ cohencyril ];
180 };
181 }
182 // lib.optionalAttrs (package != "single") {
183 passthru = lib.mapAttrs (package: deps: metacoq_ package) packages;
184 }
185 )).overrideAttrs
186 (
187 o:
188 let
189 requiresOcamlStdlibShims =
190 lib.versionAtLeast o.version "1.0-8.16"
191 || (o.version == "dev" && (lib.versionAtLeast coq.coq-version "8.16" || coq.coq-version == "dev"));
192 in
193 {
194 propagatedBuildInputs =
195 o.propagatedBuildInputs ++ lib.optional requiresOcamlStdlibShims coq.ocamlPackages.stdlib-shims;
196 }
197 );
198 # utils, common, template-pcuic, quotation, safechecker-plugin, and erasure-plugin
199 # packages didn't exist before 1.2, so building nothing in that case
200 patched-derivation = derivation.overrideAttrs (
201 o:
202 lib.optionalAttrs
203 (
204 o.pname != null
205 && lib.elem package [
206 "utils"
207 "common"
208 "template-pcuic"
209 "quotation"
210 "safechecker-plugin"
211 "erasure-plugin"
212 ]
213 && o.version != null
214 && o.version != "dev"
215 && lib.versions.isLt "1.2" o.version
216 )
217 {
218 patchPhase = "";
219 configurePhase = "";
220 preBuild = "";
221 buildPhase = "echo doing nothing";
222 installPhase = "echo doing nothing";
223 }
224 );
225 in
226 patched-derivation;
227in
228metacoq_ (if single then "single" else "all")