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