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