tjh.dev
nixpkgs mirror (for testing)
github.com/NixOS/nixpkgs
nix
1{
2 lib,
3 mkCoqDerivation,
4 mathcomp,
5 mathcomp-finmap,
6 mathcomp-bigenough,
7 hierarchy-builder,
8 stdlib,
9 single ? false,
10 coq,
11 version ? null,
12}@args:
13
14let
15 repo = "analysis";
16 owner = "math-comp";
17
18 release."1.14.0".sha256 = "sha256-FFcfxnF1wtz2e9Rdqu4Wd0rtLW0DYoXswCTji//RSCQ=";
19 release."1.13.0".sha256 = "sha256-nn2gl6cAO93QEdMvLGlB9WAPddQiOdeRtk1pLO+gxII=";
20 release."1.12.0".sha256 = "sha256-PF10NlZ+aqP3PX7+UsZwgJT9PEaDwzvrS/ZGzjP64Wo=";
21 release."1.11.0".sha256 = "sha256-1apbzBvaLNw/8ARLUhGGy89CyXW+/6O4ckdxKPraiVc=";
22 release."1.9.0".sha256 = "sha256-zj7WSDUg8ISWxcipGpjEwvvnLp1g8nm23BZiib/15+g=";
23 release."1.8.0".sha256 = "sha256-2ZafDmZAwGB7sxdUwNIE3xvwBRw1kFDk0m5Vz+onWZc=";
24 release."1.7.0".sha256 = "sha256-GgsMIHqLkWsPm2VyOPeZdOulkN00IoBz++qA6yE9raQ=";
25 release."1.5.0".sha256 = "sha256-EWogrkr5TC5F9HjQJwO3bl4P8mij8U7thUGJNNI+k88=";
26 release."1.4.0".sha256 = "sha256-eDggeuEU0fMK7D5FbxvLkbAgpLw5lwL/Rl0eLXAnJeg=";
27 release."1.2.0".sha256 = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo=";
28 release."1.1.0".sha256 = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o=";
29 release."1.0.0".sha256 = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4=";
30 release."0.7.0".sha256 = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60=";
31 release."0.6.7".sha256 = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA=";
32 release."0.6.6".sha256 = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
33 release."0.6.5".sha256 = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
34 release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
35 release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
36 release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
37 release."0.5.2".sha256 = "0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw";
38 release."0.5.1".sha256 = "1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68";
39 release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
40 release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
41 release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
42 release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
43 release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
44 release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
45 release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
46 release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
47
48 defaultVersion =
49 let
50 case = coq: mc: out: {
51 cases = [
52 coq
53 mc
54 ];
55 inherit out;
56 };
57 in
58 with lib.versions;
59 lib.switch
60 [ coq.coq-version mathcomp.version ]
61 [
62 (case (range "8.20" "9.1") (range "2.4.0" "2.5.0") "1.14.0")
63 (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.13.0")
64 (case (range "8.20" "9.1") (range "2.1.0" "2.4.0") "1.12.0")
65 (case (range "8.19" "8.20") (range "2.1.0" "2.3.0") "1.9.0")
66 (case (range "8.17" "8.20") (range "2.0.0" "2.2.0") "1.1.0")
67 (case (range "8.17" "8.19") (range "1.17.0" "1.19.0") "0.7.0")
68 (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.7")
69 (case (range "8.17" "8.18") (range "1.15.0" "1.18.0") "0.6.6")
70 (case (range "8.14" "8.18") (range "1.15.0" "1.17.0") "0.6.5")
71 (case (range "8.14" "8.18") (range "1.13.0" "1.16.0") "0.6.1")
72 (case (range "8.14" "8.18") (range "1.13" "1.15") "0.5.2")
73 (case (range "8.13" "8.15") (range "1.13" "1.14") "0.5.1")
74 (case (range "8.13" "8.15") (range "1.12" "1.14") "0.3.13")
75 (case (range "8.11" "8.14") (range "1.12" "1.13") "0.3.10")
76 (case (range "8.10" "8.12") "1.11.0" "0.3.3")
77 (case (range "8.10" "8.11") "1.11.0" "0.3.1")
78 (case (range "8.8" "8.11") (range "1.8" "1.10") "0.2.3")
79 ]
80 null;
81
82 # list of analysis packages sorted by dependency order
83 packages = {
84 "classical" = [ ];
85 "reals" = [ "classical" ];
86 "experimental-reals" = [ "reals" ];
87 "analysis" = [ "reals" ];
88 "reals-stdlib" = [ "reals" ];
89 "analysis-stdlib" = [
90 "analysis"
91 "reals-stdlib"
92 ];
93 };
94
95 mathcomp_ =
96 package:
97 let
98 classical-deps = [
99 mathcomp.ssreflect
100 mathcomp.algebra
101 mathcomp-finmap
102 ];
103 experimental-reals-deps = [ mathcomp-bigenough ];
104 analysis-deps = [
105 mathcomp.field
106 mathcomp-bigenough
107 ];
108 intra-deps = lib.optionals (package != "single") (map mathcomp_ packages.${package});
109 pkgpath = lib.switch package [
110 {
111 case = "single";
112 out = ".";
113 }
114 {
115 case = "analysis";
116 out = "theories";
117 }
118 {
119 case = "experimental-reals";
120 out = "experimental_reals";
121 }
122 {
123 case = "reals-stdlib";
124 out = "reals_stdlib";
125 }
126 {
127 case = "analysis-stdlib";
128 out = "analysis_stdlib";
129 }
130 ] package;
131 pname = if package == "single" then "mathcomp-analysis-single" else "mathcomp-${package}";
132 derivation = mkCoqDerivation {
133 inherit
134 version
135 pname
136 defaultVersion
137 release
138 repo
139 owner
140 ;
141
142 namePrefix = [
143 "coq"
144 "mathcomp"
145 ];
146
147 propagatedBuildInputs =
148 intra-deps
149 ++ lib.optionals (lib.elem package [
150 "classical"
151 "single"
152 ]) classical-deps
153 ++ lib.optionals (lib.elem package [
154 "experimental-reals"
155 "single"
156 ]) experimental-reals-deps
157 ++ lib.optionals (lib.elem package [
158 "analysis"
159 "single"
160 ]) analysis-deps
161 ++ lib.optional (lib.elem package [
162 "reals-stdlib"
163 "analysis-stdlib"
164 "single"
165 ]) stdlib;
166
167 preBuild = ''
168 cd ${pkgpath}
169 '';
170
171 meta = {
172 description = "Analysis library compatible with Mathematical Components";
173 maintainers = [ lib.maintainers.cohencyril ];
174 license = lib.licenses.cecill-c;
175 };
176
177 passthru = lib.mapAttrs (package: deps: mathcomp_ package) packages;
178 };
179 # split packages didn't exist before 0.6, so building nothing in that case
180 patched-derivation1 = derivation.overrideAttrs (
181 o:
182 lib.optionalAttrs
183 (
184 o.pname != null
185 && o.pname != "mathcomp-analysis"
186 && o.version != null
187 && o.version != "dev"
188 && lib.versions.isLt "0.6" o.version
189 )
190 {
191 preBuild = "";
192 buildPhase = "echo doing nothing";
193 installPhase = "echo doing nothing";
194 }
195 );
196 patched-derivation2 = patched-derivation1.overrideAttrs (
197 o:
198 lib.optionalAttrs (
199 o.pname != null
200 && o.pname == "mathcomp-analysis"
201 && o.version != null
202 && o.version != "dev"
203 && lib.versions.isLt "0.6" o.version
204 ) { preBuild = ""; }
205 );
206 # only packages classical and analysis existed before 1.7, so building nothing in that case
207 patched-derivation3 = patched-derivation2.overrideAttrs (
208 o:
209 lib.optionalAttrs
210 (
211 o.pname != null
212 && o.pname != "mathcomp-classical"
213 && o.pname != "mathcomp-analysis"
214 && o.version != null
215 && o.version != "dev"
216 && lib.versions.isLt "1.7" o.version
217 )
218 {
219 preBuild = "";
220 buildPhase = "echo doing nothing";
221 installPhase = "echo doing nothing";
222 }
223 );
224 patched-derivation = patched-derivation3.overrideAttrs (
225 o:
226 lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
227 {
228 propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
229 }
230 );
231 in
232 patched-derivation;
233in
234# this is just a wrapper for rocqPackages.mathcomp-analysis for Rocq >= 9.0
235if
236 coq.rocqPackages ? mathcomp-analysis
237 && !(lib.elem version [
238 "1.12.0"
239 "1.13.0"
240 "1.14.0"
241 "1.15.0"
242 ])
243then
244 coq.rocqPackages.mathcomp-analysis.override {
245 inherit version single;
246 inherit
247 mathcomp
248 mathcomp-finmap
249 mathcomp-bigenough
250 stdlib
251 ;
252 inherit (coq.rocqPackages) rocq-core;
253 }
254else
255 mathcomp_ (if single then "single" else "analysis")