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# (boot order fingroup algebra solvable field character). They can be #
5# accessed individually through the passthrough attributes of mathcomp #
6# bearing the same names (mathcomp.boot, 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/rocq.section.md. #
11############################################################################
12
13{
14 lib,
15 ncurses,
16 graphviz,
17 lua,
18 fetchzip,
19 mkRocqDerivation,
20 withDoc ? false,
21 single ? false,
22 rocq-core,
23 hierarchy-builder,
24 version ? null,
25}@args:
26
27let
28 repo = "mathcomp";
29 owner = "math-comp";
30 withDoc = single && (args.withDoc or false);
31 defaultVersion =
32 let
33 case = case: out: { inherit case out; };
34 inherit (lib.versions) range;
35 in
36 lib.switch rocq-core.rocq-version [
37 (case (range "9.0" "9.1") "2.5.0")
38 ] null;
39 release = {
40 "2.5.0".sha256 = "sha256-M/6IP4WhTQ4j2Bc8nXBXjSjWO08QzNIYI+a2owfOh+8=";
41 };
42 releaseRev = v: "mathcomp-${v}";
43
44 # list of core mathcomp packages sorted by dependency order
45 packages = {
46 "boot" = [ ];
47 "order" = [ "boot" ];
48 "fingroup" = [ "boot" ];
49 "algebra" = [
50 "order"
51 "fingroup"
52 ];
53 "solvable" = [ "algebra" ];
54 "field" = [ "solvable" ];
55 "character" = [ "field" ];
56 "all" = [ "character" ];
57 };
58
59 mathcomp_ =
60 package:
61 let
62 mathcomp-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
63 pkgpath = if package == "single" then "." else package;
64 pname = if package == "single" then "mathcomp" else "mathcomp-${package}";
65 pkgallMake = ''
66 echo "all.v" > Make
67 echo "-I ." >> Make
68 echo "-R . mathcomp.all" >> Make
69 '';
70 derivation = mkRocqDerivation (
71 {
72 inherit
73 version
74 pname
75 defaultVersion
76 release
77 releaseRev
78 repo
79 owner
80 ;
81
82 nativeBuildInputs = lib.optionals withDoc [
83 graphviz
84 lua
85 ];
86 buildInputs = [ ncurses ];
87 propagatedBuildInputs = mathcomp-deps ++ [ hierarchy-builder ];
88
89 buildFlags = lib.optional withDoc "doc";
90
91 preBuild = ''
92 if [[ -f etc/buildlibgraph ]]
93 then patchShebangs etc/buildlibgraph
94 fi
95 ''
96 + ''
97 cd ${pkgpath}
98 ''
99 + lib.optionalString (package == "all") pkgallMake;
100
101 meta = {
102 homepage = "https://math-comp.github.io/";
103 license = lib.licenses.cecill-b;
104 maintainers = with lib.maintainers; [
105 vbgl
106 jwiegley
107 cohencyril
108 ];
109 };
110 }
111 // lib.optionalAttrs (package != "single") { passthru = lib.mapAttrs (p: _: mathcomp_ p) packages; }
112 // lib.optionalAttrs withDoc {
113 htmldoc_template = fetchzip {
114 url = "https://github.com/math-comp/math-comp.github.io/archive/doc-1.12.0.zip";
115 sha256 = "0y1352ha2yy6k2dl375sb1r68r1qi9dyyy7dyzj5lp9hxhhq69x8";
116 };
117 postBuild = ''
118 cp -rf _build_doc/* .
119 rm -r _build_doc
120 '';
121 postInstall =
122 let
123 tgt = "$out/share/coq/${rocq-core.rocq-version}/";
124 in
125 lib.optionalString withDoc ''
126 mkdir -p ${tgt}
127 cp -r htmldoc ${tgt}
128 cp -r $htmldoc_template/htmldoc_template/* ${tgt}/htmldoc/
129 '';
130 buildTargets = "doc";
131 extraInstallFlags = [ "-f Makefile.coq" ];
132 }
133 );
134 # patched-derivation1 = derivation.overrideAttrs ...
135 in
136 derivation;
137in
138mathcomp_ (if single then "single" else "all")