Skip to content

Commit 132ff3f

Browse files
proux01proux01
committed
[CI] Test Nix overlay
1 parent e6e1b60 commit 132ff3f

1 file changed

Lines changed: 123 additions & 0 deletions

File tree

‎.nix/coq-overlays/mathcomp-analysis/default.nix‎

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

0 commit comments

Comments
 (0)