tjh.dev
1{ lib,
2 mkCoqDerivation,
3 mathcomp, mathcomp-finmap, mathcomp-bigenough,
4 hierarchy-builder,
5 single ? false,
6 coqPackages, coq, version ? null }@args:
7
8let
9 repo = "analysis";
10 owner = "math-comp";
11
12 release."1.2.0".sha256 = "sha256-w6BivDM4dF4Iv4rUTy++2feweNtMAJxgGExPfYGhXxo=";
13 release."1.1.0".sha256 = "sha256-wl4kZf4mh9zbFfGcqaFEgWRyp0Bj511F505mYodpS6o=";
14 release."1.0.0".sha256 = "sha256-KiXyaWB4zQ3NuXadq4BSWfoN1cIo1xiLVSN6nW03tC4=";
15 release."0.7.0".sha256 = "sha256-JwkyetXrFsFHqz8KY3QBpHsrkhmEFnrCGuKztcoen60=";
16 release."0.6.7".sha256 = "sha256-3i2PBMEwihwgwUmnS0cmrZ8s+aLPFVq/vo0aXMUaUyA=";
17 release."0.6.6".sha256 = "sha256-tWtv6yeB5/vzwpKZINK9OQ0yQsvD8qu9zVSNHvLMX5Y=";
18 release."0.6.5".sha256 = "sha256-oJk9/Jl1SWra2aFAXRAVfX7ZUaDfajqdDksYaW8dv8E=";
19 release."0.6.1".sha256 = "sha256-1VyNXu11/pDMuH4DmFYSUF/qZ4Bo+/Zl3Y0JkyrH/r0=";
20 release."0.6.0".sha256 = "sha256-0msICcIrK6jbOSiBu0gIVU3RHwoEEvB88CMQqW/06rg=";
21 release."0.5.3".sha256 = "sha256-1NjFsi5TITF8ZWx1NyppRmi8g6YaoUtTdS9bU/sUe5k=";
22 release."0.5.2".sha256 = "0yx5p9zyl8jv1vg7rgkyq8dqzkdnkqv969mi62whmhkvxbavgzbw";
23 release."0.5.1".sha256 = "1hnzqb1gxf88wgj2n1b0f2xm6sxg9j0735zdsv6j12hlvx5lwk68";
24 release."0.3.13".sha256 = "sha256-Yaztew79KWRC933kGFOAUIIoqukaZOdNOdw4XszR1Hg=";
25 release."0.3.10".sha256 = "sha256-FBH2c8QRibq5Ycw/ieB8mZl0fDiPrYdIzZ6W/A3pIhI=";
26 release."0.3.9".sha256 = "sha256-uUU9diBwUqBrNRLiDc0kz0CGkwTZCUmigPwLbpDOeg4=";
27 release."0.3.6".sha256 = "0g2j7b2hca4byz62ssgg90bkbc8wwp7xkb2d3225bbvihi92b4c5";
28 release."0.3.4".sha256 = "18mgycjgg829dbr7ps77z6lcj03h3dchjbj5iir0pybxby7gd45c";
29 release."0.3.3".sha256 = "1m2mxcngj368vbdb8mlr91hsygl430spl7lgyn9qmn3jykack867";
30 release."0.3.1".sha256 = "1iad288yvrjv8ahl9v18vfblgqb1l5z6ax644w49w9hwxs93f2k8";
31 release."0.2.3".sha256 = "0p9mr8g1qma6h10qf7014dv98ln90dfkwn76ynagpww7qap8s966";
32
33 defaultVersion = let inherit (lib.versions) range; in
34 lib.switch [ coq.version mathcomp.version ] [
35 { cases = [ (range "8.17" "8.20") (range "2.0.0" "2.2.0") ]; out = "1.1.0"; }
36 { cases = [ (range "8.17" "8.19") (range "1.17.0" "1.19.0") ]; out = "0.7.0"; }
37 { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.7"; }
38 { cases = [ (range "8.17" "8.18") (range "1.15.0" "1.18.0") ]; out = "0.6.6"; }
39 { cases = [ (range "8.14" "8.18") (range "1.15.0" "1.17.0") ]; out = "0.6.5"; }
40 { cases = [ (range "8.14" "8.18") (range "1.13.0" "1.16.0") ]; out = "0.6.1"; }
41 { cases = [ (range "8.14" "8.18") (range "1.13" "1.15") ]; out = "0.5.2"; }
42 { cases = [ (range "8.13" "8.15") (range "1.13" "1.14") ]; out = "0.5.1"; }
43 { cases = [ (range "8.13" "8.15") (range "1.12" "1.14") ]; out = "0.3.13"; }
44 { cases = [ (range "8.11" "8.14") (range "1.12" "1.13") ]; out = "0.3.10"; }
45 { cases = [ (range "8.10" "8.12") "1.11.0" ]; out = "0.3.3"; }
46 { cases = [ (range "8.10" "8.11") "1.11.0" ]; out = "0.3.1"; }
47 { cases = [ (range "8.8" "8.11") (range "1.8" "1.10") ]; out = "0.2.3"; }
48 ] null;
49
50 # list of analysis packages sorted by dependency order
51 packages = [ "classical" "analysis" ];
52
53 mathcomp_ = package: let
54 classical-deps = [ mathcomp.algebra mathcomp-finmap ];
55 analysis-deps = [ mathcomp.field mathcomp-bigenough ];
56 intra-deps = lib.optionals (package != "single") (map mathcomp_ (lib.head (lib.splitList (lib.pred.equal package) packages)));
57 pkgpath = if package == "single" then "."
58 else if package == "analysis" then "theories" else "${package}";
59 pname = if package == "single" then "mathcomp-analysis-single"
60 else "mathcomp-${package}";
61 derivation = mkCoqDerivation ({
62 inherit version pname defaultVersion release repo owner;
63
64 namePrefix = [ "coq" "mathcomp" ];
65
66 propagatedBuildInputs =
67 intra-deps
68 ++ lib.optionals (lib.elem package [ "classical" "single" ]) classical-deps
69 ++ lib.optionals (lib.elem package [ "analysis" "single" ]) analysis-deps;
70
71 preBuild = ''
72 cd ${pkgpath}
73 '';
74
75 meta = {
76 description = "Analysis library compatible with Mathematical Components";
77 maintainers = [ lib.maintainers.cohencyril ];
78 license = lib.licenses.cecill-c;
79 };
80
81 passthru = lib.genAttrs packages mathcomp_;
82 });
83 # split packages didn't exist before 0.6, so bulding nothing in that case
84 patched-derivation1 = derivation.overrideAttrs (o:
85 lib.optionalAttrs (o.pname != null && o.pname != "mathcomp-analysis" &&
86 o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version)
87 { preBuild = ""; buildPhase = "echo doing nothing"; installPhase = "echo doing nothing"; }
88 );
89 patched-derivation2 = patched-derivation1.overrideAttrs (o:
90 lib.optionalAttrs (o.pname != null && o.pname == "mathcomp-analysis" &&
91 o.version != null && o.version != "dev" && lib.versions.isLt "0.6" o.version)
92 { preBuild = ""; }
93 );
94 patched-derivation = patched-derivation2.overrideAttrs (o:
95 lib.optionalAttrs (o.version != null
96 && (o.version == "dev" || lib.versions.isGe "0.3.4" o.version))
97 {
98 propagatedBuildInputs = o.propagatedBuildInputs ++ [ hierarchy-builder ];
99 }
100 );
101 in patched-derivation;
102in
103mathcomp_ (if single then "single" else "analysis")