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