tjh.dev
1############################################################################
2# This file mainly provides the `mathcomp` derivation, which is #
3# essentially a meta-package containing all core mathcomp libraries #
4# (ssreflect fingroup algebra solvable field character). They can be #
5# accessed individually through the passthrough attributes of mathcomp #
6# bearing the same names (mathcomp.ssreflect, etc). #
7############################################################################
8# Compiling a custom version of mathcomp using `mathcomp.override`. #
9# This is the replacement for the former `mathcomp_ config` function. #
10# See the documentation at doc/languages-frameworks/coq.section.md. #
11############################################################################
12
13{
14 lib,
15 ncurses,
16 graphviz,
17 lua,
18 fetchzip,
19 mkCoqDerivation,
20 withDoc ? false,
21 single ? false,
22 coq,
23 hierarchy-builder,
24 stdlib,
25 version ? null,
26}@args:
27
28let
29 repo = "math-comp";
30 owner = "math-comp";
31 withDoc = single && (args.withDoc or false);
32 defaultVersion =
33 let
34 inherit (lib.versions) range;
35 in
36 lib.switch coq.coq-version [
37 {
38 case = range "8.20" "9.0";
39 out = "2.4.0";
40 }
41 {
42 case = range "8.19" "9.0";
43 out = "2.3.0";
44 }
45 {
46 case = range "8.17" "8.20";
47 out = "2.2.0";
48 }
49 {
50 case = range "8.17" "8.18";
51 out = "2.1.0";
52 }
53 {
54 case = range "8.17" "8.18";
55 out = "2.0.0";
56 }
57 {
58 case = range "8.19" "8.20";
59 out = "1.19.0";
60 }
61 {
62 case = range "8.17" "8.18";
63 out = "1.18.0";
64 }
65 {
66 case = range "8.15" "8.18";
67 out = "1.17.0";
68 }
69 {
70 case = range "8.13" "8.18";
71 out = "1.16.0";
72 }
73 {
74 case = range "8.14" "8.16";
75 out = "1.15.0";
76 }
77 {
78 case = range "8.11" "8.15";
79 out = "1.14.0";
80 }
81 {
82 case = range "8.11" "8.15";
83 out = "1.13.0";
84 }
85 {
86 case = range "8.10" "8.13";
87 out = "1.12.0";
88 }
89 {
90 case = range "8.7" "8.12";
91 out = "1.11.0";
92 }
93 {
94 case = range "8.7" "8.11";
95 out = "1.10.0";
96 }
97 {
98 case = range "8.7" "8.11";
99 out = "1.9.0";
100 }
101 {
102 case = range "8.7" "8.9";
103 out = "1.8.0";
104 }
105 {
106 case = range "8.6" "8.9";
107 out = "1.7.0";
108 }
109 {
110 case = range "8.5" "8.7";
111 out = "1.6.4";
112 }
113 ] null;
114 release = {
115 "2.4.0".sha256 = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
116 "2.3.0".sha256 = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
117 "2.2.0".sha256 = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
118 "2.1.0".sha256 = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
119 "2.0.0".sha256 = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
120 "1.19.0".sha256 = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
121 "1.18.0".sha256 = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
122 "1.17.0".sha256 = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
123 "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
124 "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
125 "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
126 "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
127 "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
128 "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
129 "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
130 "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
131 "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
132 "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
133 "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
134 "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
135 };
136 releaseRev = v: "mathcomp-${v}";
137
138 # list of core mathcomp packages sorted by dependency order
139 packages = {
140 "boot" = [ ];
141 "order" = [ "boot" ];
142 "fingroup" = [ "boot" ];
143 "ssreflect" = [
144 "boot"
145 "order"
146 ];
147 "algebra" = [
148 "order"
149 "fingroup"
150 ];
151 "solvable" = [ "algebra" ];
152 "field" = [ "solvable" ];
153 "character" = [ "field" ];
154 "all" = [ "character" ];
155 };
156
157 mathcomp_ =
158 package:
159 let
160 mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
161 pkgpath = if package == "single" then "." else package;
162 pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
163 pkgallMake = ''
164 echo "all.v" > Make
165 echo "-I ." >> Make
166 echo "-R . mathcomp.all" >> Make
167 '';
168 derivation = mkCoqDerivation (
169 {
170 inherit
171 version
172 pname
173 defaultVersion
174 release
175 releaseRev
176 repo
177 owner
178 ;
179
180 mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
181 nativeBuildInputs = lib.optionals withDoc [
182 graphviz
183 lua
184 ];
185 buildInputs = [ ncurses ];
186 propagatedBuildInputs = mathcomp-deps;
187
188 buildFlags = lib.optional withDoc "doc";
189
190 preBuild =
191 ''
192 if [[ -f etc/utils/ssrcoqdep ]]
193 then patchShebangs etc/utils/ssrcoqdep
194 fi
195 if [[ -f etc/buildlibgraph ]]
196 then patchShebangs etc/buildlibgraph
197 fi
198 ''
199 + ''
200 # handle mathcomp < 2.4.0 which had an extra base mathcomp directory
201 test -d mathcomp && cd mathcomp
202 cd ${pkgpath} || cd ssreflect # before 2.5, boot didn't exist, make it behave as ssreflect
203 ''
204 + lib.optionalString (package == "all") pkgallMake;
205
206 meta = {
207 homepage = "https://math-comp.github.io/";
208 license = lib.licenses.cecill-b;
209 maintainers = with lib.maintainers; [
210 vbgl
211 jwiegley
212 cohencyril
213 ];
214 };
215 }
216 // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
217 // lib.optionalAttrs withDoc {
218 htmldoc_template = fetchzip {
219 url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
220 sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
221 };
222 postBuild = ''
223 cp -rf _build_doc/* .
224 rm -r _build_doc
225 '';
226 postInstall =
227 let
228 tgt = "$out/share/coq/${coq.coq-version}/";
229 in
230 lib.optionalString withDoc ''
231 mkdir -p ${tgt}
232 cp -r htmldoc ${tgt}
233 cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
234 '';
235 buildTargets = "doc";
236 extraInstallFlags = [ "-f Makefile.coq" ];
237 }
238 );
239 patched-derivation1 = derivation.overrideAttrs (
240 o:
241 lib.optionalAttrs
242 (
243 o.pname != null
244 && o.pname == "mathcomp-all"
245 && o.version != null
246 && o.version != "dev"
247 && lib.versions.isLt "1.7" o.version
248 )
249 {
250 preBuild = "";
251 buildPhase = "";
252 installPhase = "echo doing nothing";
253 }
254 );
255 patched-derivation2 = patched-derivation1.overrideAttrs (
256 o:
257 lib.optionalAttrs
258 (
259 lib.versions.isLe "8.7" coq.coq-version || (o.version != "dev" && lib.versions.isLe "1.7" o.version)
260 )
261 {
262 installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
263 }
264 );
265 patched-derivation3 = patched-derivation2.overrideAttrs (
266 o:
267 lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
268 {
269 propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
270 }
271 );
272 patched-derivation4 = patched-derivation3.overrideAttrs (
273 o:
274 lib.optionalAttrs (o.version != null && o.version == "2.3.0") {
275 propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
276 }
277 );
278 # boot and order packages didn't exist before 2.5,
279 # so make boot behave as ssreflect then (c.f., above)
280 # and building nothing in order and ssreflect
281 patched-derivation5 = patched-derivation4.overrideAttrs (
282 o:
283 lib.optionalAttrs
284 (
285 lib.elem package [
286 "order"
287 "ssreflect"
288 ]
289 && o.version != null
290 && o.version != "dev"
291 && lib.versions.isLt "2.5" o.version
292 )
293 {
294 preBuild = "";
295 buildPhase = "echo doing nothing";
296 installPhase = "echo doing nothing";
297 }
298 );
299 in
300 patched-derivation5;
301in
302mathcomp_ (if single then "single" else "all")