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{ lib, ncurses, graphviz, lua, fetchzip,
14 mkCoqDerivation, withDoc ? false, single ? false,
15 coqPackages, coq, hierarchy-builder, version ? null }@args:
16
17let
18 repo = "math-comp";
19 owner = "math-comp";
20 withDoc = single && (args.withDoc or false);
21 defaultVersion = let inherit (lib.versions) range; in
22 lib.switch coq.coq-version [
23 { case = range "8.19" "8.20"; out = "1.19.0"; }
24 { case = range "8.17" "8.18"; out = "1.18.0"; }
25 { case = range "8.15" "8.18"; out = "1.17.0"; }
26 { case = range "8.16" "8.20"; out = "2.2.0"; }
27 { case = range "8.16" "8.18"; out = "2.1.0"; }
28 { case = range "8.16" "8.18"; out = "2.0.0"; }
29 { case = range "8.13" "8.18"; out = "1.16.0"; }
30 { case = range "8.14" "8.16"; out = "1.15.0"; }
31 { case = range "8.11" "8.15"; out = "1.14.0"; }
32 { case = range "8.11" "8.15"; out = "1.13.0"; }
33 { case = range "8.10" "8.13"; out = "1.12.0"; }
34 { case = range "8.7" "8.12"; out = "1.11.0"; }
35 { case = range "8.7" "8.11"; out = "1.10.0"; }
36 { case = range "8.7" "8.11"; out = "1.9.0"; }
37 { case = range "8.7" "8.9"; out = "1.8.0"; }
38 { case = range "8.6" "8.9"; out = "1.7.0"; }
39 { case = range "8.5" "8.7"; out = "1.6.4"; }
40 ] null;
41 release = {
42 "2.2.0".sha256 = "sha256-SPyWSI5kIP5w7VpgnQ4vnK56yEuWnJylNQOT7M77yoQ=";
43 "2.1.0".sha256 = "sha256-XDLx0BIkVRkSJ4sGCIE51j3rtkSGemNTs/cdVmTvxqo=";
44 "2.0.0".sha256 = "sha256-dpOmrHYUXBBS9kmmz7puzufxlbNpIZofpcTvJFLG5DI=";
45 "1.19.0".sha256 = "sha256-3kxS3qA+7WwQkXoFC/+kq3OEkv4kMEzQ/G3aXPsp1Q4=";
46 "1.18.0".sha256 = "sha256-mJJ/zvM2WtmBZU3U4oid/zCMvDXei/93v5hwyyqwiiY=";
47 "1.17.0".sha256 = "sha256-bUfoSTMiW/GzC1jKFay6DRqGzKPuLOSUsO6/wPSFwNg=";
48 "1.16.0".sha256 = "sha256-gXTKhRgSGeRBUnwdDezMsMKbOvxdffT+kViZ9e1gEz0=";
49 "1.15.0".sha256 = "1bp0jxl35ms54s0mdqky15w9af03f3i0n06qk12k4gw1xzvwqv21";
50 "1.14.0".sha256 = "07yamlp1c0g5nahkd2gpfhammcca74ga2s6qr7a3wm6y6j5pivk9";
51 "1.13.0".sha256 = "0j4cz2y1r1aw79snkcf1pmicgzf8swbaf9ippz0vg99a572zqzri";
52 "1.12.0".sha256 = "1ccfny1vwgmdl91kz5xlmhq4wz078xm4z5wpd0jy5rn890dx03wp";
53 "1.11.0".sha256 = "06a71d196wd5k4wg7khwqb7j7ifr7garhwkd54s86i0j7d6nhl3c";
54 "1.10.0".sha256 = "1b9m6pwxxyivw7rgx82gn5kmgv2mfv3h3y0mmjcjfypi8ydkrlbv";
55 "1.9.0".sha256 = "0lid9zaazdi3d38l8042lczb02pw5m9wq0yysiilx891hgq2p81r";
56 "1.8.0".sha256 = "07l40is389ih8bi525gpqs3qp4yb2kl11r9c8ynk1ifpjzpnabwp";
57 "1.7.0".sha256 = "0wnhj9nqpx2bw6n1l4i8jgrw3pjajvckvj3lr4vzjb3my2lbxdd1";
58 "1.6.4".sha256 = "09ww48qbjsvpjmy1g9yhm0rrkq800ffq21p6fjkbwd34qvd82raz";
59 "1.6.1".sha256 = "1ilw6vm4dlsdv9cd7kmf0vfrh2kkzr45wrqr8m37miy0byzr4p9i";
60 };
61 releaseRev = v: "mathcomp-${v}";
62
63 # list of core mathcomp packages sorted by dependency order
64 packages = [ "ssreflect" "fingroup" "algebra" "solvable" "field" "character" "all" ];
65
66 mathcomp_ = package: let
67 mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages)));
68 pkgpath = if package == "single" then "mathcomp" else "mathcomp/${package}";
69 pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
70 pkgallMake = ''
71 echo "all.v" > Make
72 echo "-I ." >> Make
73 echo "-R . mathcomp.all" >> Make
74 '';
75 derivation = mkCoqDerivation ({
76 inherit version pname defaultVersion release releaseRev repo owner;
77
78 mlPlugin = lib.versions.isLe "8.6" coq.coq-version;
79 nativeBuildInputs = lib.optionals withDoc [ graphviz lua ];
80 buildInputs = [ ncurses ];
81 propagatedBuildInputs = mathcomp-deps;
82
83 buildFlags = lib.optional withDoc "doc";
84
85 preBuild = ''
86 if [[ -f etc/utils/ssrcoqdep ]]
87 then patchShebangs etc/utils/ssrcoqdep
88 fi
89 if [[ -f etc/buildlibgraph ]]
90 then patchShebangs etc/buildlibgraph
91 fi
92 '' + ''
93 cd ${pkgpath}
94 '' + lib.optionalString (package == "all") pkgallMake;
95
96 meta = {
97 homepage = "https://math-comp.github.io/";
98 license = lib.licenses.cecill-b;
99 maintainers = with lib.maintainers; [ vbgl jwiegley cohencyril ];
100 };
101 } // lib.optionalAttrs (package != "single")
102 { passthru = lib.genAttrs packages mathcomp_; }
103 // lib.optionalAttrs withDoc {
104 htmldoc_template =
105 fetchzip {
106 url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
107 sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
108 };
109 postBuild = ''
110 cp -rf _build_doc/* .
111 rm -r _build_doc
112 '';
113 postInstall =
114 let tgt = "$out/share/coq/${coq.coq-version}/"; in
115 lib.optionalString withDoc ''
116 mkdir -p ${tgt}
117 cp -r htmldoc ${tgt}
118 cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
119 '';
120 buildTargets = "doc";
121 extraInstallFlags = [ "-f Makefile.coq" ];
122 });
123 patched-derivation1 = derivation.overrideAttrs (o:
124 lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-all" &&
125 o.version != null && o.version != "dev" && lib.versions.isLt "1.7" o.version)
126 { preBuild = ""; buildPhase = ""; installPhase = "echo doing nothing"; }
127 );
128 patched-derivation2 = patched-derivation1.overrideAttrs (o:
129 lib.optionalAttrs (lib.versions.isLe "8.7" coq.coq-version ||
130 (o.version != "dev" && lib.versions.isLe "1.7" o.version))
131 {
132 installFlags = o.installFlags ++ [ "-f Makefile.coq" ];
133 }
134 );
135 patched-derivation = patched-derivation2.overrideAttrs (o:
136 lib.optionalAttrs (o.version != null
137 && (o.version == "dev" || lib.versions.isGe "2.0.0" o.version))
138 {
139 propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
140 }
141 );
142 in patched-derivation;
143in
144mathcomp_ (if single then "single" else "all")