Skip to content

Commit d082af3

Browse files
proux01proux01
committed
[CI] Test equation update (now uses dune)
1 parent 8326e6a commit d082af3

File tree

2 files changed

+139
-0
lines changed

2 files changed

+139
-0
lines changed

‎.nix/config.nix

+1
Original file line numberDiff line numberDiff line change
@@ -223,6 +223,7 @@ with builtins; with (import <nixpkgs> {}).lib;
223223
coq-hammer.override.version = "31442e8178a5d85a9f57a323b65bf9f719ded8ec";
224224
coq-hammer-tactics.override.version = "31442e8178a5d85a9f57a323b65bf9f719ded8ec";
225225
equations.override.version = "3431c88a7575a3972191c25809c563aafdc6414e";
226+
equations.override.useDune = "false";
226227
equations-test.override.version = "3431c88a7575a3972191c25809c563aafdc6414e";
227228
fiat-parsers.job = false; # broken
228229
metacoq.override.version = "17ba45ffc84d37e187ef87a55b840890f1d87f01";

‎.nix/coq-overlays/equations/default.nix

+138
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,138 @@
1+
{
2+
lib,
3+
mkCoqDerivation,
4+
coq,
5+
stdlib,
6+
version ? null,
7+
}:
8+
9+
(mkCoqDerivation {
10+
pname = "equations";
11+
owner = "mattam82";
12+
repo = "Coq-Equations";
13+
opam-name = "rocq-equations";
14+
inherit version;
15+
defaultVersion = lib.switch coq.coq-version [
16+
{
17+
case = "8.20";
18+
out = "1.3.1+8.20";
19+
}
20+
{
21+
case = "8.19";
22+
out = "1.3+8.19";
23+
}
24+
{
25+
case = "8.18";
26+
out = "1.3+8.18";
27+
}
28+
{
29+
case = "8.17";
30+
out = "1.3+8.17";
31+
}
32+
{
33+
case = "8.16";
34+
out = "1.3+8.16";
35+
}
36+
{
37+
case = "8.15";
38+
out = "1.3+8.15";
39+
}
40+
{
41+
case = "8.14";
42+
out = "1.3+8.14";
43+
}
44+
{
45+
case = "8.13";
46+
out = "1.3+8.13";
47+
}
48+
{
49+
case = "8.12";
50+
out = "1.2.4+coq8.12";
51+
}
52+
{
53+
case = "8.11";
54+
out = "1.2.4+coq8.11";
55+
}
56+
{
57+
case = "8.10";
58+
out = "1.2.1+coq8.10-2";
59+
}
60+
{
61+
case = "8.9";
62+
out = "1.2.1+coq8.9";
63+
}
64+
{
65+
case = "8.8";
66+
out = "1.2+coq8.8";
67+
}
68+
{
69+
case = "8.7";
70+
out = "1.0+coq8.7";
71+
}
72+
{
73+
case = "8.6";
74+
out = "1.0+coq8.6";
75+
}
76+
] null;
77+
78+
release."1.0+coq8.6".version = "1.0";
79+
release."1.0+coq8.6".rev = "v1.0";
80+
release."1.0+coq8.6".sha256 = "19ylw9v9g35607w4hm86j7mmkghh07hmkc1ls5bqlz3dizh5q4pj";
81+
release."1.0+coq8.7".version = "1.0";
82+
release."1.0+coq8.7".rev = "v1.0-8.7";
83+
release."1.0+coq8.7".sha256 = "1bavg4zl1xn0jqrdq8iw7xqzdvdf39ligj9saz5m9c507zri952h";
84+
release."1.2+coq8.8".version = "1.2";
85+
release."1.2+coq8.8".rev = "v1.2-8.8";
86+
release."1.2+coq8.8".sha256 = "06452fyzalz7zcjjp73qb7d6xvmqb6skljkivf8pfm55fsc8s7kx";
87+
release."1.2.1+coq8.9".version = "1.2.1";
88+
release."1.2.1+coq8.9".rev = "v1.2.1-8.9";
89+
release."1.2.1+coq8.9".sha256 = "0d8ddj6nc6p0k25cd8fs17cq427zhzbc3v9pk2wd2fnvk70nlfij";
90+
release."1.2.1+coq8.10-2".version = "1.2.1";
91+
release."1.2.1+coq8.10-2".rev = "v1.2.1-8.10-2";
92+
release."1.2.1+coq8.10-2".sha256 = "0j3z4l5nrbyi9zbbyqkc6kassjanwld2188mwmrbqspaypm2ys68";
93+
release."1.2.3+coq8.11".version = "1.2.3";
94+
release."1.2.3+coq8.11".rev = "v1.2.3-8.11";
95+
release."1.2.3+coq8.11".sha256 = "1srxz1rws8jsh7402g2x2vcqgjbbsr64dxxj5d2zs48pmhb20csf";
96+
release."1.2.3+coq8.12".version = "1.2.3";
97+
release."1.2.3+coq8.12".rev = "v1.2.3-8.12";
98+
release."1.2.3+coq8.12".sha256 = "1y0jkvzyz5ssv5vby41p1i8zs7nsdc8g3pzyq73ih9jz8h252643";
99+
release."1.2.4+coq8.11".rev = "v1.2.4-8.11";
100+
release."1.2.4+coq8.11".sha256 = "01fihyav8jbjinycgjc16adpa0zy5hcav5mlkf4s9zvqxka21i52";
101+
release."1.2.4+coq8.12".rev = "v1.2.4-8.12";
102+
release."1.2.4+coq8.12".sha256 = "1n0w8is464qcq8mk2mv7amaf0khbjz5mpc9phf0rhpjm0lb22cb3";
103+
release."1.2.4+coq8.13".rev = "v1.2.4-8.13";
104+
release."1.2.4+coq8.13".sha256 = "0i014lshsdflzw6h0qxra9d2f0q82vffxv2f29awbb9ad0p4rq4q";
105+
release."1.3+8.13".rev = "v1.3-8.13";
106+
release."1.3+8.13".sha256 = "1jwjbkkkk4bwf6pz4zzz8fy5bb17aqyf4smkja59rgj9ya6nrdhg";
107+
release."1.3+8.14".rev = "v1.3-8.14";
108+
release."1.3+8.14".sha256 = "19bj9nncd1r9g4273h5qx35gs3i4bw5z9bhjni24b413hyj55hkv";
109+
release."1.3+8.15".rev = "v1.3-8.15";
110+
release."1.3+8.15".sha256 = "1vfcfpsp9zyj0sw0cwibk76nj6n0r6gwh8m1aa3lbvc0b1kbm32k";
111+
release."1.3+8.16".rev = "v1.3-8.16";
112+
release."1.3+8.16".sha256 = "sha256-zyMGeRObtSGWh7n3WCqesBZL5EgLvKwmnTy09rYpxyE=";
113+
release."1.3+8.17".rev = "v1.3-8.17";
114+
release."1.3+8.17".sha256 = "sha256-yNotSIxFkhTg3reZIchGQ7cV9WmTJ7p7hPfKGBiByDw=";
115+
release."1.3+8.18".rev = "v1.3-8.18";
116+
release."1.3+8.18".sha256 = "sha256-8MZO9vWdr8wlAov0lBTYMnde0RuMyhaiM99zp7Zwfao=";
117+
release."1.3+8.19".rev = "v1.3-8.19";
118+
release."1.3+8.19".sha256 = "sha256-roBCWfAHDww2Z2JbV5yMI3+EOfIsv3WvxEcUbBiZBsk=";
119+
release."1.3.1+8.20".rev = "v1.3.1-8.20";
120+
release."1.3.1+8.20".sha256 = "sha256-u8LB1KiACM5zVaoL7dSdHYvZgX7pf30VuqtjLLGuTzc=";
121+
122+
mlPlugin = true;
123+
124+
useDuneifVersion = v: lib.versions.isGe "1.3.1+9.0" v || v == "dev";
125+
126+
propagatedBuildInputs = [ stdlib ];
127+
128+
meta = with lib; {
129+
homepage = "https://mattam82.github.io/Coq-Equations/";
130+
description = "Plugin for Coq to add dependent pattern-matching";
131+
maintainers = with maintainers; [ jwiegley ];
132+
};
133+
}).overrideAttrs
134+
(o: {
135+
preBuild = "coq_makefile -f _CoqProject -o Makefile${
136+
lib.optionalString (lib.versionAtLeast o.version "1.2.1" || o.version == "dev") ".coq"
137+
}";
138+
})

0 commit comments

Comments
 (0)