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