Skip to content

Commit beee312

Browse files
authored
Merge pull request #114 from proux01/ci-update
[CI] Update Nix toolbox
2 parents e64810d + d66a297 commit beee312

File tree

19 files changed

+1814
-329
lines changed

19 files changed

+1814
-329
lines changed

.github/workflows/nix-action-rocq-9.0.yml

Lines changed: 177 additions & 124 deletions
Large diffs are not rendered by default.

.github/workflows/nix-action-rocq-master.yml

Lines changed: 224 additions & 148 deletions
Large diffs are not rendered by default.

.nix/config.nix

Lines changed: 28 additions & 12 deletions
Original file line numberDiff line numberDiff line change
@@ -116,7 +116,7 @@ with builtins; with (import <nixpkgs> {}).lib;
116116
"coqprime"
117117
"coquelicot"
118118
"coqutil"
119-
"coq-elpi-test"
119+
"coq-elpi"
120120
"ExtLib"
121121
"coq-hammer"
122122
"coq-hammer-tactics"
@@ -143,10 +143,18 @@ with builtins; with (import <nixpkgs> {}).lib;
143143
"json"
144144
"kami"
145145
"mathcomp"
146+
"mathcomp-algebra"
147+
"mathcomp-algebra-tactics"
146148
"mathcomp-analysis"
147149
"mathcomp-bigenough"
150+
"mathcomp-character"
148151
"mathcomp-classical"
152+
"mathcomp-field"
153+
"mathcomp-fingroup"
149154
"mathcomp-finmap"
155+
"mathcomp-reals"
156+
"mathcomp-solvable"
157+
"mathcomp-ssreflect"
150158
"mathcomp-test"
151159
"mathcomp-zify"
152160
"math-classes"
@@ -188,32 +196,39 @@ with builtins; with (import <nixpkgs> {}).lib;
188196
"metacoq"
189197
"metacoq-test"
190198
];
191-
common-bundles = listToAttrs (forEach master (p:
199+
coq-common-bundles = listToAttrs (forEach master (p:
192200
{ name = p; value.override.version = "master"; }))
193201
// listToAttrs (forEach coq-master (p:
194202
{ name = p; value.override.version = "coq-master"; }))
195203
// listToAttrs (forEach main (p:
196204
{ name = p; value.override.version = "main"; }))
197205
// {
206+
coq-elpi.override.elpi-version = "2.0.7";
198207
fiat-crypto-legacy.override.version = "sp2019latest";
199208
tlc.override.version = "master-for-coq-ci";
200209
smtcoq-trakt.override.version = "with-trakt-coq-master";
201210
coq-tools.override.version = "proux01:coq_19955";
202-
stdlib-html.job = true;
203211
stdlib-refman-html.job = true;
212+
};
213+
common-bundles = {
214+
bignums.override.version = "master";
215+
rocq-elpi.override.version = "master";
216+
rocq-elpi.override.elpi-version = "2.0.7";
217+
rocq-elpi-test.override.version = "master";
218+
stdlib-html.job = true;
204219
stdlib-test.job = true;
205220
stdlib-subcomponents.job = true;
206221
};
207222
in {
208-
"rocq-master".coqPackages = common-bundles // {
223+
"rocq-master" = { rocqPackages = common-bundles // {
224+
rocq-core.override.version = "master";
225+
}; coqPackages = coq-common-bundles // {
209226
coq.override.version = "master";
210-
coq-elpi.override.version = "master";
211-
coq-elpi.override.elpi-version = "2.0.7";
212-
};
213-
"rocq-9.0".coqPackages = common-bundles // {
214-
coq.override.version = "V9.0+rc1";
215-
coq-elpi.override.version = "master";
216-
coq-elpi.override.elpi-version = "2.0.7";
227+
}; };
228+
"rocq-9.0" = { rocqPackages = common-bundles // {
229+
rocq-core.override.version = "9.0";
230+
}; coqPackages = coq-common-bundles // {
231+
coq.override.version = "9.0";
217232
# plugin pins, from v9.0 branch of Coq
218233
aac-tactics.override.version = "109af844f39bf541823271e45e42e40069f3c2c4";
219234
atbr.override.version = "47ac8fb6bf244d9a4049e04c01e561191490f543";
@@ -240,6 +255,7 @@ with builtins; with (import <nixpkgs> {}).lib;
240255
stalmarck-tactic.override.version = "d32acd3c477c57b48dd92bdd96d53fb8fa628512";
241256
unicoq.override.version = "a9b72f755539c0b3280e38e778a09e2b7519a51a";
242257
waterproof.override.version = "443f794ddc102309d00f1d512ab50b84fdc261aa";
243-
};
258+
compcert.job = false; # broken
259+
}; };
244260
};
245261
}

.nix/coq-nix-toolbox.nix

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"ee1cc6946f9f33dd281f74cd5c5273786f0e0850"
1+
"5bb0f8deadacc9b0cf5adf5ea22a9ed360d36f8a"
Lines changed: 165 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,165 @@
1+
{
2+
lib,
3+
mkCoqDerivation,
4+
which,
5+
coq,
6+
rocqPackages,
7+
stdlib,
8+
version ? null,
9+
elpi-version ? null,
10+
}:
11+
12+
let
13+
default-elpi-version = if elpi-version != null then elpi-version else (
14+
lib.switch coq.coq-version [
15+
{ case = "8.11"; out = "1.11.4"; }
16+
{ case = "8.12"; out = "1.12.0"; }
17+
{ case = "8.13"; out = "1.13.7"; }
18+
{ case = "8.14"; out = "1.13.7"; }
19+
{ case = "8.15"; out = "1.15.0"; }
20+
{ case = "8.16"; out = "1.17.0"; }
21+
{ case = "8.17"; out = "1.17.0"; }
22+
{ case = "8.18"; out = "1.18.1"; }
23+
{ case = "8.19"; out = "1.18.1"; }
24+
{ case = "8.20"; out = "1.19.2"; }
25+
{ case = "9.0"; out = "2.0.7"; }
26+
] { }
27+
);
28+
elpi = coq.ocamlPackages.elpi.override { version = default-elpi-version; };
29+
propagatedBuildInputs_wo_elpi = [
30+
coq.ocamlPackages.findlib
31+
];
32+
derivation = mkCoqDerivation {
33+
pname = "elpi";
34+
repo = "coq-elpi";
35+
owner = "LPCIC";
36+
inherit version;
37+
defaultVersion = lib.switch coq.coq-version [
38+
{ case = "dev"; out = "master"; }
39+
{ case = "9.0"; out = "2.5.0"; }
40+
{ case = "8.20"; out = "2.2.0"; }
41+
{ case = "8.19"; out = "2.0.1"; }
42+
{ case = "8.18"; out = "2.0.0"; }
43+
{ case = "8.17"; out = "1.18.0"; }
44+
{ case = "8.16"; out = "1.15.6"; }
45+
{ case = "8.15"; out = "1.14.0"; }
46+
{ case = "8.14"; out = "1.11.2"; }
47+
{ case = "8.13"; out = "1.11.1"; }
48+
{ case = "8.12"; out = "1.8.3_8.12"; }
49+
{ case = "8.11"; out = "1.6.3_8.11"; }
50+
] null;
51+
release."2.5.0".sha256 = "sha256-Z5xjO83X/ZoTQlWnVupGXPH3HuJefr57Kv128I0dltg=";
52+
release."2.4.0".sha256 = "sha256-W2+vVGExLLux8e0nSZESSoMVvrLxhL6dmXkb+JuKiqc=";
53+
release."2.2.0".sha256 = "sha256-rADEoqTXM7/TyYkUKsmCFfj6fjpWdnZEOK++5oLfC/I=";
54+
release."2.0.1".sha256 = "sha256-cuoPsEJ+JRLVc9Golt2rJj4P7lKltTrrmQijjoViooc=";
55+
release."2.0.0".sha256 = "sha256-A/cH324M21k3SZ7+YWXtaYEbu6dZQq3K0cb1RMKjbsM=";
56+
release."1.19.0".sha256 = "sha256-kGoo61nJxeG/BqV+iQaV3iinwPStND+7+fYMxFkiKrQ=";
57+
release."1.18.0".sha256 = "sha256-2fCOlhqi4YkiL5n8SYHuc3pLH+DArf9zuMH7IhpBc2Y=";
58+
release."1.17.0".sha256 = "sha256-J8GatRKFU0ekNCG3V5dBI+FXypeHcLgC5QJYGYzFiEM=";
59+
release."1.15.6".sha256 = "sha256-qc0q01tW8NVm83801HHOBHe/7H1/F2WGDbKO6nCXfno=";
60+
release."1.15.1".sha256 = "sha256-NT2RlcIsFB9AvBhMxil4ZZIgx+KusMqDflj2HgQxsZg=";
61+
release."1.14.0".sha256 = "sha256:1v2p5dlpviwzky2i14cj7gcgf8cr0j54bdm9fl5iz1ckx60j6nvp";
62+
release."1.13.0".sha256 = "1j7s7dlnjbw222gnbrsjgmjck1yrx7h6hwm8zikcyxi0zys17w7n";
63+
release."1.12.1".sha256 = "sha256-4mO6/co7NcIQSGIQJyoO8lNWXr6dqz+bIYPO/G0cPkY=";
64+
release."1.11.2".sha256 = "0qk5cfh15y2zrja7267629dybd3irvxk1raz7z8qfir25a81ckd4";
65+
release."1.11.1".sha256 = "10j076vc2hdcbm15m6s7b6xdzibgfcbzlkgjnlkr2vv9k13qf8kc";
66+
release."1.10.1".sha256 = "1zsyx26dvj7pznfd2msl2w7zbw51q1nsdw0bdvdha6dga7ijf7xk";
67+
release."1.9.7".sha256 = "0rvn12h9dpk9s4pxy32p8j0a1h7ib7kg98iv1cbrdg25y5vs85n1";
68+
release."1.9.5".sha256 = "0gjdwmb6bvb5gh0a6ra48bz5fb3pr5kpxijb7a8mfydvar5i9qr6";
69+
release."1.9.4".sha256 = "0nii7238mya74f9g6147qmpg6gv6ic9b54x5v85nb6q60d9jh0jq";
70+
release."1.9.3".sha256 = "198irm800fx3n8n56vx1c6f626cizp1d7jfkrc6ba4iqhb62ma0z";
71+
release."1.9.2".sha256 = "1rr2fr8vjkc0is7vh1461aidz2iwkigdkp6bqss4hhv0c3ijnn07";
72+
release."1.8.3_8.12".sha256 = "15z2l4zy0qpw0ws7bvsmpmyv543aqghrfnl48nlwzn9q0v89p557";
73+
release."1.8.3_8.12".version = "1.8.3";
74+
release."1.8.2_8.12".sha256 = "1n6jwcdazvjgj8vsv2r9zgwpw5yqr5a1ndc2pwhmhqfl04b5dk4y";
75+
release."1.8.2_8.12".version = "1.8.2";
76+
release."1.8.1".sha256 = "1fbbdccdmr8g4wwpihzp4r2xacynjznf817lhijw6kqfav75zd0r";
77+
release."1.8.0".sha256 = "13ywjg94zkbki22hx7s4gfm9rr87r4ghsgan23xyl3l9z8q0idd1";
78+
release."1.7.0".sha256 = "1ws5cqr0xawv69prgygbl3q6dgglbaw0vc397h9flh90kxaqgyh8";
79+
release."1.6.3_8.11".sha256 = "1j340cr2bv95clzzkkfmsjkklham1mj84cmiyprzwv20q89zr1hp";
80+
release."1.6.3_8.11".version = "1.6.3";
81+
release."1.6.2_8.11".sha256 = "06xrx0ljilwp63ik2sxxr7h617dgbch042xfcnfpy5x96br147rn";
82+
release."1.6.2_8.11".version = "1.6.2";
83+
release."1.6.1_8.11".sha256 = "0yyyh35i1nb3pg4hw7cak15kj4y6y9l84nwar9k1ifdsagh5zq53";
84+
release."1.6.1_8.11".version = "1.6.1";
85+
release."1.6.0_8.11".sha256 = "0ahxjnzmd7kl3gl38kyjqzkfgllncr2ybnw8bvgrc6iddgga7bpq";
86+
release."1.6.0_8.11".version = "1.6.0";
87+
release."1.6.0".sha256 = "0kf99i43mlf750fr7fric764mm495a53mg5kahnbp6zcjcxxrm0b";
88+
releaseRev = v: "v${v}";
89+
90+
buildFlags = [ "OCAMLWARN=" ];
91+
92+
mlPlugin = true;
93+
useDuneifVersion = v: lib.versions.isGe "2.2.0" v || v == "dev";
94+
95+
propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [ elpi ];
96+
97+
preConfigure = ''
98+
make elpi/dune || true
99+
'';
100+
101+
meta = {
102+
description = "Coq plugin embedding ELPI";
103+
maintainers = [ lib.maintainers.cohencyril ];
104+
license = lib.licenses.lgpl21Plus;
105+
};
106+
};
107+
patched-derivation1 = derivation.overrideAttrs
108+
(
109+
o:
110+
lib.optionalAttrs (o ? elpi-version)
111+
{
112+
propagatedBuildInputs = propagatedBuildInputs_wo_elpi ++ [
113+
(coq.ocamlPackages.elpi.override { version = o.elpi-version; })
114+
];
115+
}
116+
);
117+
patched-derivation2 = patched-derivation1.overrideAttrs
118+
(
119+
o:
120+
lib.optionalAttrs (o.version != null && (o.version == "dev" || lib.versions.isGe "2.2.0" o.version))
121+
{
122+
propagatedBuildInputs = o.propagatedBuildInputs ++ [ coq.ocamlPackages.ppx_optcomp ];
123+
}
124+
);
125+
patched-derivation3 = patched-derivation2.overrideAttrs
126+
(
127+
o:
128+
lib.optionalAttrs (o.version != null && o.version == "2.4.0")
129+
{
130+
propagatedBuildInputs = o.propagatedBuildInputs ++ [ stdlib ];
131+
}
132+
);
133+
patched-derivation4 = patched-derivation3.overrideAttrs
134+
(
135+
o:
136+
# this is just a wrapper for rocPackages.rocq-elpi for Rocq >= 9.0
137+
if coq.version != null && (coq.version == "dev"
138+
|| lib.versions.isGe "9.0" coq.version) then {
139+
configurePhase = ''
140+
echo no configuration
141+
'';
142+
buildPhase = ''
143+
echo building nothing
144+
'';
145+
installPhase = ''
146+
echo installing nothing
147+
'';
148+
propagatedBuildInputs = o.propagatedBuildInputs
149+
++ [ rocqPackages.rocq-elpi ];
150+
} else lib.optionalAttrs (o.version != null && (o.version == "dev"
151+
|| lib.versions.isGe "2.5.0" o.version)) {
152+
configurePhase = ''
153+
make dune-files || true
154+
'';
155+
buildPhase = ''
156+
dune build -p rocq-elpi @install ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
157+
'';
158+
installPhase = ''
159+
dune install --root . rocq-elpi --prefix=$out --libdir $OCAMLFIND_DESTDIR
160+
mkdir $out/lib/coq/
161+
mv $OCAMLFIND_DESTDIR/coq $out/lib/coq/${coq.coq-version}
162+
'';
163+
}
164+
);
165+
in patched-derivation4
Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
1-
{ lib, mkCoqDerivation, coq, mathcomp-algebra, version ? null }:
1+
{ lib, mkCoqDerivation, coq, mathcomp-algebra, stdlib, version ? null }:
22

33
mkCoqDerivation {
44
pname = "fcsl-pcm";
55
owner = "imdea-software";
66
inherit version;
77
defaultVersion = null; # no released version
88

9-
propagatedBuildInputs = [ mathcomp-algebra ];
9+
propagatedBuildInputs = [ mathcomp-algebra stdlib ];
1010
}

.nix/coq-overlays/jasmin/default.nix

Lines changed: 0 additions & 12 deletions
This file was deleted.

.nix/coq-overlays/stdlib-refman-html/default.nix

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,7 +3,8 @@
33
coqPackages.lib.overrideCoqDerivation {
44
pname = "stdlib-refman-html";
55

6-
overrideBuildInputs = stdlib.buildInputs ++ [ coq.ocamlPackages.ocaml coq.ocamlPackages.dune_3 stdlib ]
6+
overrideBuildInputs = stdlib.buildInputs
7+
++ [ coq.ocamlPackages.ocaml coq.ocamlPackages.dune_3 stdlib ]
78
++ [
89
# Sphinx doc dependencies
910
(python311.withPackages
@@ -13,11 +14,16 @@ coqPackages.lib.overrideCoqDerivation {
1314
];
1415

1516
buildPhase = ''
17+
patchShebangs dev/with-rocq-wrap.sh
1618
dev/with-rocq-wrap.sh dune build --root . --no-buffer @refman-html ''${enableParallelBuilding:+-j $NIX_BUILD_CORES}
1719
'';
1820

1921
installPhase = ''
2022
echo "nothing to install"
2123
touch $out
2224
'';
25+
26+
fixupPhase = ''
27+
echo "nothing to fixup"
28+
'';
2329
} stdlib

.nix/coq-overlays/trakt/default.nix

Lines changed: 48 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,48 @@
1+
{
2+
lib,
3+
mkCoqDerivation,
4+
coq,
5+
coq-elpi,
6+
stdlib,
7+
version ? null,
8+
}:
9+
10+
mkCoqDerivation {
11+
pname = "trakt";
12+
owner = "ecranceMERCE";
13+
14+
release."1.0".sha256 = "sha256-Qhw5fWFYxUFO2kIWWz/og+4fuy9aYG27szfNk3IglhY=";
15+
release."1.1".sha256 = "sha256-JmrtM9WcT8Bfy0WZCw8xdubuMomyXmfLXJwpnCNrvsg=";
16+
release."1.2".sha256 = "sha256-YQRtK2MjjsMlytdu9iutUDKhwOo4yWrSwhyBb2zNHoE=";
17+
release."1.2+8.13".sha256 = "sha256-hozms4sPSMr4lFkJ20x+uW9Wqt067bifnPQxdGyKhQQ=";
18+
19+
inherit version;
20+
defaultVersion =
21+
with lib.versions;
22+
lib.switch
23+
[ coq.version ]
24+
[
25+
{
26+
cases = [ (range "8.15" "8.17") ];
27+
out = "1.2";
28+
}
29+
{
30+
cases = [ (isEq "8.13") ];
31+
out = "1.2+8.13";
32+
}
33+
{
34+
cases = [ (range "8.13" "8.17") ];
35+
out = "1.1";
36+
}
37+
]
38+
null;
39+
40+
propagatedBuildInputs = [ coq-elpi stdlib ];
41+
42+
meta = with lib; {
43+
description = "Generic goal preprocessing tool for proof automation tactics in Coq";
44+
maintainers = with maintainers; [ siraben ];
45+
license = licenses.lgpl3Plus;
46+
platforms = platforms.unix;
47+
};
48+
}

.nix/coq-overlays/coq-elpi-test/default.nix renamed to .nix/rocq-overlays/rocq-elpi-test/default.nix

Lines changed: 6 additions & 7 deletions
Original file line numberDiff line numberDiff line change
@@ -1,20 +1,19 @@
1-
{ mkCoqDerivation, coq-elpi, version ? null }:
1+
{ mkRocqDerivation, rocq-elpi, version ? null }:
22

3-
mkCoqDerivation {
4-
pname = "coq-elpi-test";
3+
mkRocqDerivation {
4+
pname = "rocq-elpi-test";
55
repo = "coq-elpi";
66
owner = "LPCIC";
77
inherit version;
88

9-
propagatedBuildInputs = [ coq-elpi ];
9+
propagatedBuildInputs = [ rocq-elpi ];
1010

1111
useDune = true;
1212

1313
buildPhase = ''
1414
export DUNE_build_FLAGS="--release"
15-
make test-core
16-
make examples
17-
make test-apps
15+
make -j1 all-tests
16+
make -j1 all-examples
1817
'';
1918

2019
installPhase = ''

0 commit comments

Comments
 (0)