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