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