Skip to content

Commit 10bbfd0

Browse files
proux01proux01
committed
Test CI
1 parent 705e9df commit 10bbfd0

File tree

20 files changed

+5699
-0
lines changed

20 files changed

+5699
-0
lines changed

‎.github/workflows/nix-action-coq-master.yml

+5,032
Large diffs are not rendered by default.

‎.nix/config.nix

+240
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,240 @@
1+
with builtins; with (import <nixpkgs> {}).lib;
2+
{
3+
## DO NOT CHANGE THIS
4+
format = "1.0.0";
5+
## unless you made an automated or manual update
6+
## to another supported format.
7+
8+
## The attribute to build from the local sources,
9+
## either using nixpkgs data or the overlays located in `.nix/coq-overlays`
10+
## Will determine the default main-job of the bundles defined below
11+
attribute = "stdlib";
12+
13+
## If you want to select a different attribute (to build from the local sources as well)
14+
## when calling `nix-shell` and `nix-build` without the `--argstr job` argument
15+
# shell-attribute = "{{nix_name}}";
16+
17+
## Maybe the shortname of the library is different from
18+
## the name of the nixpkgs attribute, if so, set it here:
19+
# pname = "{{shortname}}";
20+
21+
## Lists the dependencies, phrased in terms of nix attributes.
22+
## No need to list Coq, it is already included.
23+
## These dependencies will systematically be added to the currently
24+
## known dependencies, if any more than Coq.
25+
## /!\ Remove this field as soon as the package is available on nixpkgs.
26+
## /!\ Manual overlays in `.nix/coq-overlays` should be preferred then.
27+
# buildInputs = [ ];
28+
29+
## Indicate the relative location of your _CoqProject
30+
## If not specified, it defaults to "_CoqProject"
31+
coqproject = "theories/_CoqProject";
32+
33+
## Cachix caches to use in CI
34+
## Below we list some standard ones
35+
cachix.coq = {};
36+
cachix.math-comp = {};
37+
# cachix.coq-community = {};
38+
39+
## If you have write access to one of these caches you can
40+
## provide the auth token or signing key through a secret
41+
## variable on GitHub. Then, you should give the variable
42+
## name here. For instance, coq-community projects can use
43+
## the following line instead of the one above:
44+
cachix.coq-community.authToken = "CACHIX_AUTH_TOKEN";
45+
46+
## Or if you have a signing key for a given Cachix cache:
47+
# cachix.my-cache.signingKey = "CACHIX_SIGNING_KEY"
48+
49+
## Note that here, CACHIX_AUTH_TOKEN and CACHIX_SIGNING_KEY
50+
## are the names of secret variables. They are set in
51+
## GitHub's web interface.
52+
53+
## select an entry to build in the following `bundles` set
54+
## defaults to "default"
55+
default-bundle = "coq-master";
56+
57+
## write one `bundles.name` attribute set per
58+
## alternative configuration
59+
## When generating GitHub Action CI, one workflow file
60+
## will be created per bundle
61+
bundles = let
62+
## In some cases, light overrides are not available/enough
63+
## in which case you can use either
64+
# coqPackages.<coq-pkg>.overrideAttrs = o: <overrides>;
65+
## or a "long" overlay to put in `.nix/coq-overlays
66+
## you may use `nix-shell --run fetchOverlay <coq-pkg>`
67+
## to automatically retrieve the one from nixpkgs
68+
## if it exists and is correctly named/located
69+
70+
## You can override Coq and other coqPackages
71+
## through the following attribute
72+
## If <ocaml-pkg> does not support light overrides,
73+
## you may use `overrideAttrs` or long overlays
74+
## located in `.nix/ocaml-overlays`
75+
## (there is no automation for this one)
76+
# ocamlPackages.<ocaml-pkg>.override.version = "x.xx";
77+
78+
## You can also override packages from the nixpkgs toplevel
79+
# <nix-pkg>.override.overrideAttrs = o: <overrides>;
80+
## Or put an overlay in `.nix/overlays`
81+
82+
## you may mark a package as a main CI job (one to take deps and
83+
## rev deps from) as follows
84+
# coqPackages.<main-pkg>.main-job = true;
85+
## by default the current package and its shell attributes are main jobs
86+
87+
## you may mark a package as a CI job as follows
88+
# coqPackages.<another-pkg>.job = "test";
89+
## It can then built through
90+
## nix-build --argstr bundle "default" --arg job "test";
91+
## in the absence of such a directive, the job "another-pkg" will
92+
## is still available, but will be automatically included in the CI
93+
## via the command genNixActions only if it is a dependency or a
94+
## reverse dependency of a job flagged as "main-job" (see above).
95+
96+
## Run on push on following branches (default [ "master" ])
97+
# push-branches = [ "master" "branch2" ];
98+
99+
master = [
100+
"stdlib"
101+
# "mathcomp" -> overlay
102+
"fourcolor"
103+
"odd-order"
104+
"mathcomp-zify"
105+
"mathcomp-finmap"
106+
"mathcomp-bigenough"
107+
"mathcomp-analysis"
108+
"unicoq"
109+
# "math-classes" -> overlay
110+
# "corn" -> overlay
111+
"stdpp"
112+
# "iris" -> overlay
113+
# "autosubst" -> overlay
114+
"iris-examples"
115+
# "coq-hammer" -> overlay
116+
# "flocq" -> overlay
117+
# "coq-performance-tests" -> overlay
118+
# TODO coq-tools
119+
"coquelicot"
120+
# "compcert" -> overlay
121+
# "vst" -> overlay
122+
# TODO cross-crypto -> Docker
123+
# TODO rewriter
124+
# TODO fiat_parsers -> Docker
125+
# TODO fiat_crypto_legacy -> Docker
126+
# TODO fiat_crypto -> Docker
127+
# TODO rupicola -> Docker
128+
# TODO bedrock2 -> Docker
129+
# TODO coqutil -> Docker
130+
# TODO kami -> Docker
131+
# TODO riscv_coq -> Docker
132+
"CoLoR"
133+
"bignums"
134+
"coqprime"
135+
# "bbv" -> overlay
136+
"coinduction"
137+
# "coq-elpi" -> overlay
138+
"hierarchy-builder"
139+
# "engine bench" -> overlay
140+
# TODO fcsl_pcm -> not ported to MC 2, to remove
141+
# "coq-ext-lib" -> overlay
142+
# "simple-io" -> overlay
143+
# "QuickChick" -> overlay
144+
"menhir"
145+
# "neural-net-coq-interp" -> overlay
146+
# "aac-tactics" -> overlay
147+
"paco"
148+
# "ITree" -> overlay
149+
"itree-io"
150+
"ceres"
151+
"parsec"
152+
# "json" -> overlay
153+
"async-test"
154+
"http"
155+
"paramcoq"
156+
# "relation-algebra" -> overlay
157+
"StructTact"
158+
"InfSeqExt"
159+
"Cheerios"
160+
"Verdi"
161+
"VerdiRaft"
162+
# TODO argosy -> Docker
163+
# "atbr" -> overlay
164+
# TODO perennial -> Docker
165+
# "sf" -> overlay
166+
"deriving"
167+
# "category-theory" -> overlay
168+
"itauto"
169+
# "smtcoq-trakt" -> overlay
170+
# "stalmarck" -> overlay
171+
# "stalmarck-tactic" -> overlay
172+
];
173+
coq-master = [
174+
"dpdgraph"
175+
# "smtcoq" -> overlay
176+
"trakt"
177+
# "waterproof" -> overlay
178+
];
179+
main = [
180+
"coq-lsp"
181+
# "equations" -> overlay
182+
# "metacoq" -> overlay
183+
# "serapi" -> overlay
184+
"mathcomp-word"
185+
# "jasmin" -> overlay
186+
];
187+
common-bundles = listToAttrs (forEach master (p:
188+
{ name = p; value.override.version = "master"; }))
189+
// listToAttrs (forEach coq-master (p:
190+
{ name = p; value.override.version = "coq-master"; }))
191+
// listToAttrs (forEach main (p:
192+
{ name = p; value.override.version = "main"; }))
193+
// {
194+
coq-elpi.override.version = "proux01:split_stdlib";
195+
mathcomp.override.version = "proux01:split_stdlib";
196+
# tlc.override.version = "master-for-coq-ci"; -> overlay
197+
tlc.override.version = "proux01:split_stdlib";
198+
flocq.override.version = "split_stdlib";
199+
coq-ext-lib.override.version = "split_stdlib";
200+
aac-tactics.override.version = "split_stdlib";
201+
coq-hammer.override.version = "proux01:split_stdlib";
202+
math-classes.override.version = "split_stdlib";
203+
corn.override.version = "split_stdlib";
204+
equations.override.version = "proux01:split_stdlib";
205+
autosubst.override.version = "split_stdlib";
206+
relation-algebra.override.version = "proux01:split_stdlib";
207+
category-theory.override.version = "proux01:split_stdlib";
208+
metacoq.override.version = "proux01:split_stdlib";
209+
compcert.override.version = "proux01:split_stdlib";
210+
simple-io.override.version = "proux01:split_stdlib";
211+
QuickChick.override.version = "proux01:split_stdlib";
212+
serapi.override.version = "proux01:coq_19310";
213+
iris.override.version = "proux:split_stdlib";
214+
vst.override.version = "proux01:split_stdlib";
215+
smtcoq.override.version = "split_stdlib";
216+
CoLoR.override.version = "proux01:split_stdlib";
217+
ITree.override.version = "proux01:split_stdlib";
218+
atbr.override.version = "split_stdlib";
219+
stalmarck.override.version = "split_stdlib";
220+
stalmarck-tactic.override.version = "split_stdlib";
221+
waterproof.override.version = "proux01:split_stdlib";
222+
smtcoq-trakt.override.version = "proux01:split_stdlib-trakt";
223+
jasmin.override.version = "proux01:split_stdlib";
224+
sf.override.version = "proux01:split_stdlib";
225+
bbv.override.version = "proux01:split_stdlib";
226+
json.override.version = "proux01:split_stdlib";
227+
neural-net-coq-interp.override.version = "proux01:split_stdlib";
228+
engine-bench.override.version = "proux01:split_stdlib";
229+
coq-performance-tests.override.version = "proux01:split_stdlib";
230+
};
231+
in {
232+
"coq-master".coqPackages = common-bundles // {
233+
coq.override.version = "proux01:split_stdlib";
234+
};
235+
"coq-master".ocamlPackages = {
236+
elpi.override.version = "1.19.2";
237+
menhirLib.override.version = "master";
238+
};
239+
};
240+
}

‎.nix/coq-nix-toolbox.nix

+1
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
"0ce5f6bcf2415aac89ce150b20499ba1e1afe76d"

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

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
{ lib, mkCoqDerivation, coq, Verdi, version ? null }:
2+
3+
mkCoqDerivation {
4+
pname = "verdi-raft";
5+
owner = "uwplse";
6+
inherit version;
7+
defaultVersion = null; # no released version
8+
9+
propagatedBuildInputs = [ Verdi ];
10+
}

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

+11
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,11 @@
1+
{ lib, mkCoqDerivation, coq, stdlib, version ? null }:
2+
3+
mkCoqDerivation {
4+
pname = "atbr";
5+
inherit version;
6+
defaultVersion = null; # no released version
7+
8+
mlPlugin = true;
9+
10+
propagatedBuildInputs = [ stdlib ];
11+
}

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

+10
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,10 @@
1+
{ lib, mkCoqDerivation, coq, stdlib, version ? null }:
2+
3+
mkCoqDerivation {
4+
pname = "bbv";
5+
owner = "mit-plv";
6+
inherit version;
7+
defaultVersion = null; # no released version
8+
9+
propagatedBuildInputs = [ stdlib ];
10+
}

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

+12
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,12 @@
1+
{ lib, mkCoqDerivation, coq, stdlib, version ? null }:
2+
3+
mkCoqDerivation {
4+
pname = "coinduction";
5+
owner = "damien-pous";
6+
inherit version;
7+
defaultVersion = null; # no released version
8+
9+
mlPlugin = true;
10+
11+
propagatedBuildInputs = [ stdlib ];
12+
}

‎.nix/coq-overlays/coq-performance-tests/default.nix

+22
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
{ lib, time, mkCoqDerivation, coq, stdlib, version ? null }:
2+
3+
mkCoqDerivation {
4+
pname = "coq-performance-tests";
5+
owner = "coq-community";
6+
inherit version;
7+
defaultVersion = null; # no released version
8+
9+
mlPlugin = true;
10+
11+
nativeBuildInputs = [ time ];
12+
propagatedBuildInputs = [ stdlib ];
13+
14+
preConfigure = ''
15+
for f in $(find . -name "*.sh") ; do patchShebangs $f ; done
16+
'';
17+
18+
buildPhase = ''
19+
make coq perf-Sanity
20+
make validate
21+
'';
22+
}

‎.nix/coq-overlays/engine-bench/default.nix

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{ lib, mkCoqDerivation, coq, stdlib, version ? null }:
2+
3+
mkCoqDerivation {
4+
pname = "engine-bench";
5+
owner = "mit-plv";
6+
inherit version;
7+
defaultVersion = null; # no released version
8+
9+
propagatedBuildInputs = [ stdlib ];
10+
11+
buildPhase = ''
12+
make coq
13+
make coq-perf-Sanity
14+
'';
15+
}

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

+37
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,37 @@
1+
{ lib, bash, autoconf, automake,
2+
mkCoqDerivation, coq, stdlib, version ? null }:
3+
4+
mkCoqDerivation {
5+
pname = "flocq";
6+
owner = "proux01";
7+
inherit version;
8+
defaultVersion = with lib.versions; lib.switch coq.coq-version [
9+
{ case = range "8.14" "8.19"; out = "4.1.4"; }
10+
{ case = range "8.14" "8.18"; out = "4.1.3"; }
11+
{ case = range "8.14" "8.17"; out = "4.1.1"; }
12+
{ case = range "8.14" "8.16"; out = "4.1.0"; }
13+
{ case = range "8.7" "8.15"; out = "3.4.3"; }
14+
{ case = range "8.5" "8.8"; out = "2.6.1"; }
15+
] null;
16+
release."4.1.4".sha256 = "sha256-Use6Mlx79yef1CkCPyGoOItsD69B9KR+mQArCtmre4s=";
17+
release."4.1.3".sha256 = "sha256-os3cI885xNpxI+1p5rb8fSNnxKr7SFxqh83+3AM3t4I=";
18+
release."4.1.1".sha256 = "sha256-FbClxlV0ZaxITe7s9SlNbpeMNDJli+Dfh2TMrjaMtHo=";
19+
release."4.1.0".sha256 = "sha256:09rak9cha7q11yfqracbcq75mhmir84331h1218xcawza48rbjik";
20+
release."3.4.3".sha256 = "sha256-YTdWlEmFJjCcHkl47jSOgrGqdXoApJY4u618ofCaCZE=";
21+
release."3.4.2".sha256 = "1s37hvxyffx8ccc8mg5aba7ivfc39p216iibvd7f2cb9lniqk1pw";
22+
release."3.3.1".sha256 = "1mk8adhi5hrllsr0hamzk91vf2405sjr4lh5brg9201mcw11abkz";
23+
release."2.6.1".sha256 = "0q5a038ww5dn72yvwn5298d3ridkcngb1dik8hdyr3xh7gr5qibj";
24+
releaseRev = v: "flocq-${v}";
25+
26+
nativeBuildInputs = [ bash autoconf ];
27+
mlPlugin = true;
28+
useMelquiondRemake.logpath = "Flocq";
29+
30+
propagatedBuildInputs = [ stdlib ];
31+
32+
meta = with lib; {
33+
description = "Floating-point formalization for the Coq system";
34+
license = licenses.lgpl3;
35+
maintainers = with maintainers; [ jwiegley ];
36+
};
37+
}

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

+15
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,15 @@
1+
{ lib, mkCoqDerivation, coq, QuickChick, async-test, version ? null }:
2+
3+
mkCoqDerivation {
4+
pname = "http";
5+
owner = "liyishuai";
6+
repo = "coq-http";
7+
inherit version;
8+
defaultVersion = null; # no released version
9+
10+
propagatedBuildInputs = [ QuickChick async-test ];
11+
12+
configurePhase = ''
13+
sed -e 's/^ install extract.*//' -i Makefile
14+
'';
15+
}

0 commit comments

Comments
 (0)