pyrox.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 case = case: out: { inherit case out; };
35 inherit (lib.versions) range;
36 in
37 lib.switch coq.coq-version [
38 (case (range "8.20" "9.1") "2.4.0")
39 (case (range "8.19" "9.0") "2.3.0")
40 (case (range "8.17" "8.20") "2.2.0")
41 (case (range "8.17" "8.18") "2.1.0")
42 (case (range "8.17" "8.18") "2.0.0")
43 (case (range "8.19" "8.20") "1.19.0")
44 (case (range "8.17" "8.18") "1.18.0")
45 (case (range "8.15" "8.18") "1.17.0")
46 (case (range "8.13" "8.18") "1.16.0")
47 (case (range "8.14" "8.16") "1.15.0")
48 (case (range "8.11" "8.15") "1.14.0")
49 (case (range "8.11" "8.15") "1.13.0")
50 (case (range "8.10" "8.13") "1.12.0")
51 (case (range "8.7" "8.12") "1.11.0")
52 (case (range "8.7" "8.11") "1.10.0")
53 (case (range "8.7" "8.11") "1.9.0")
54 (case (range "8.7" "8.9") "1.8.0")
55 (case (range "8.6" "8.9") "1.7.0")
56 (case (range "8.5" "8.7") "1.6.4")
57 ] null;
58 release = {
59 "2.4.0".sha256 = "sha256-A1XgLLwZRvKS8QyceCkSQa7ue6TYyf5fMft5gSx9NOs=";
60 "2.3.0".sha256 = "sha256-wa6OBig8rhAT4iwupSylyCAMhO69rADa0MQIX5zzL+Q=";
61 "2.2.0".sha256 = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
62 "2.1.0".sha256 = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
63 "2.0.0".sha256 = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
64 "1.19.0".sha256 = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
65 "1.18.0".sha256 = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
66 "1.17.0".sha256 = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
67 "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
68 "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
69 "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
70 "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
71 "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
72 "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
73 "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
74 "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
75 "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
76 "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
77 "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
78 "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
79 };
80 releaseRev = v: "mathcomp-${v}";
81
82 # list of core mathcomp packages sorted by dependency order
83 packages = {
84 "boot" = [ ];
85 "order" = [ "boot" ];
86 "fingroup" = [ "boot" ];
87 "ssreflect" = [
88 "boot"
89 "order"
90 ];
91 "algebra" = [
92 "order"
93 "fingroup"
94 ];
95 "solvable" = [ "algebra" ];
96 "field" = [ "solvable" ];
97 "character" = [ "field" ];
98 "all" = [ "character" ];
99 };
100
101 mathcomp_ =
102 package:
103 let
104 mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
105 pkgpath = if package == "single" then "." else package;
106 pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
107 pkgallMake = ''
108 echo "all.v" > Make
109 echo "-I ." >> Make
110 echo "-R . mathcomp.all" >> Make
111 '';
112 derivation = mkCoqDerivation (
113 {
114 inherit
115 version
116 pname
117 defaultVersion
118 release
119 releaseRev
120 repo
121 owner
122 ;
123
124 mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
125 nativeBuildInputs = lib.optionals withDoc [
126 graphviz
127 lua
128 ];
129 buildInputs = [ ncurses ];
130 propagatedBuildInputs = mathcomp-deps;
131
132 buildFlags = lib.optional withDoc "doc";
133
134 preBuild = ''
135 if [[ -f etc/utils/ssrcoqdep ]]
136 then patchShebangs etc/utils/ssrcoqdep
137 fi
138 if [[ -f etc/buildlibgraph ]]
139 then patchShebangs etc/buildlibgraph
140 fi
141 ''
142 + ''
143 # handle mathcomp < 2.4.0 which had an extra base mathcomp directory
144 test -d mathcomp && cd mathcomp
145 cd ${pkgpath} || cd ssreflect # before 2.5, boot didn't exist, make it behave as ssreflect
146 ''
147 + lib.optionalString (package == "all") pkgallMake;
148
149 meta = {
150 homepage = "https://math-comp.github.io/";
151 license = lib.licenses.cecill-b;
152 maintainers = with lib.maintainers; [
153 vbgl
154 jwiegley
155 cohencyril
156 ];
157 };
158 }
159 // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
160 // lib.optionalAttrs withDoc {
161 htmldoc_template = fetchzip {
162 url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
163 sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
164 };
165 postBuild = ''
166 cp -rf _build_doc/* .
167 rm -r _build_doc
168 '';
169 postInstall =
170 let
171 tgt = "$out/share/coq/${coq.coq-version}/";
172 in
173 lib.optionalString withDoc ''
174 mkdir -p ${tgt}
175 cp -r htmldoc ${tgt}
176 cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
177 '';
178 buildTargets = "doc";
179 extraInstallFlags = [ "-f Makefile.coq" ];
180 }
181 );
182 patched-derivation1 = derivation.overrideAttrs (
183 o:
184 lib.optionalAttrs
185 (
186 o.pname != null
187 && o.pname == "mathcomp-all"
188 && o.version != null
189 && o.version != "dev"
190 && lib.versions.isLt "1.7" o.version
191 )
192 {
193 preBuild = "";
194 buildPhase = "";
195 installPhase = "echo doing nothing";
196 }
197 );
198 patched-derivation2 = patched-derivation1.overrideAttrs (
199 o:
200 lib.optionalAttrs
201 (
202 lib.versions.isLe "8.7" coq.coq-version || (o.version != "dev" && lib.versions.isLe "1.7" o.version)
203 )
204 {
205 installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
206 }
207 );
208 patched-derivation3 = patched-derivation2.overrideAttrs (
209 o:
210 lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
211 {
212 propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
213 }
214 );
215 patched-derivation4 = patched-derivation3.overrideAttrs (
216 o:
217 lib.optionalAttrs (o.version != null && o.version == "2.3.0") {
218 propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
219 }
220 );
221 # boot and order packages didn't exist before 2.5,
222 # so make boot behave as ssreflect then (c.f., above)
223 # and building nothing in order and ssreflect
224 patched-derivation5 = patched-derivation4.overrideAttrs (
225 o:
226 lib.optionalAttrs
227 (
228 lib.elem package [
229 "order"
230 "ssreflect"
231 ]
232 && o.version != null
233 && o.version != "dev"
234 && lib.versions.isLt "2.5" o.version
235 )
236 {
237 preBuild = "";
238 buildPhase = "echo doing nothing";
239 installPhase = "echo doing nothing";
240 }
241 );
242 in
243 patched-derivation5;
244in
245mathcomp_ (if single then "single" else "all")