Skip to content

Commit 84e409d

Browse files
garesgares
authored
Merge pull request #765 from proux01/ci-coqeal
[CI] Readd coqeal
2 parents 7ee951d + eb28a9e commit 84e409d

File tree

5 files changed

+297
-2
lines changed

5 files changed

+297
-2
lines changed

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,83 @@ jobs:
248248
name: Building/fetching current CI target
249249
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
250250
--argstr job "coq-elpi"
251+
coqeal:
252+
needs:
253+
- coq
254+
- mathcomp-algebra
255+
- multinomials
256+
- mathcomp-real-closed
257+
runs-on: ubuntu-latest
258+
steps:
259+
- name: Determine which commit to initially checkout
260+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
261+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
262+
}}\" >> $GITHUB_ENV\nfi\n"
263+
- name: Git checkout
264+
uses: actions/checkout@v4
265+
with:
266+
fetch-depth: 0
267+
ref: ${{ env.target_commit }}
268+
- name: Determine which commit to test
269+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
270+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
271+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
272+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
273+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
274+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
275+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
276+
\ fi\nfi\n"
277+
- name: Git checkout
278+
uses: actions/checkout@v4
279+
with:
280+
fetch-depth: 0
281+
ref: ${{ env.tested_commit }}
282+
- name: Cachix install
283+
uses: cachix/install-nix-action@v30
284+
with:
285+
nix_path: nixpkgs=channel:nixpkgs-unstable
286+
- name: Cachix setup coq-elpi
287+
uses: cachix/cachix-action@v15
288+
with:
289+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
290+
extraPullNames: coq, coq-community, math-comp
291+
name: coq-elpi
292+
- id: stepGetDerivation
293+
name: Getting derivation for current job (coqeal)
294+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
295+
\"coq-8.20\" --argstr job \"coqeal\" \\\n --dry-run 2> err > out || (touch
296+
fail; true)\n"
297+
- name: Error reporting
298+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
299+
- name: Failure check
300+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
301+
- id: stepCheck
302+
name: Checking presence of CI target for current job
303+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
304+
- if: steps.stepCheck.outputs.status == 'built'
305+
name: 'Building/fetching previous CI target: coq'
306+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
307+
--argstr job "coq"
308+
- if: steps.stepCheck.outputs.status == 'built'
309+
name: 'Building/fetching previous CI target: mathcomp-algebra'
310+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
311+
--argstr job "mathcomp-algebra"
312+
- if: steps.stepCheck.outputs.status == 'built'
313+
name: 'Building/fetching previous CI target: bignums'
314+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
315+
--argstr job "bignums"
316+
- if: steps.stepCheck.outputs.status == 'built'
317+
name: 'Building/fetching previous CI target: multinomials'
318+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
319+
--argstr job "multinomials"
320+
- if: steps.stepCheck.outputs.status == 'built'
321+
name: 'Building/fetching previous CI target: mathcomp-real-closed'
322+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
323+
--argstr job "mathcomp-real-closed"
324+
- if: steps.stepCheck.outputs.status == 'built'
325+
name: Building/fetching current CI target
326+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
327+
--argstr job "coqeal"
251328
coquelicot:
252329
needs:
253330
- coq

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

Lines changed: 141 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,67 @@
11
jobs:
2+
bignums:
3+
needs:
4+
- coq
5+
- stdlib
6+
runs-on: ubuntu-latest
7+
steps:
8+
- name: Determine which commit to initially checkout
9+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
10+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
11+
}}\" >> $GITHUB_ENV\nfi\n"
12+
- name: Git checkout
13+
uses: actions/checkout@v4
14+
with:
15+
fetch-depth: 0
16+
ref: ${{ env.target_commit }}
17+
- name: Determine which commit to test
18+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
19+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
20+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
21+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
22+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
23+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
24+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
25+
\ fi\nfi\n"
26+
- name: Git checkout
27+
uses: actions/checkout@v4
28+
with:
29+
fetch-depth: 0
30+
ref: ${{ env.tested_commit }}
31+
- name: Cachix install
32+
uses: cachix/install-nix-action@v30
33+
with:
34+
nix_path: nixpkgs=channel:nixpkgs-unstable
35+
- name: Cachix setup coq-elpi
36+
uses: cachix/cachix-action@v15
37+
with:
38+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
39+
extraPullNames: coq, coq-community, math-comp
40+
name: coq-elpi
41+
- id: stepGetDerivation
42+
name: Getting derivation for current job (bignums)
43+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
44+
\"coq-master\" --argstr job \"bignums\" \\\n --dry-run 2> err > out || (touch
45+
fail; true)\n"
46+
- name: Error reporting
47+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
48+
- name: Failure check
49+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
50+
- id: stepCheck
51+
name: Checking presence of CI target for current job
52+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
53+
- if: steps.stepCheck.outputs.status == 'built'
54+
name: 'Building/fetching previous CI target: coq'
55+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
56+
--argstr job "coq"
57+
- if: steps.stepCheck.outputs.status == 'built'
58+
name: 'Building/fetching previous CI target: stdlib'
59+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
60+
--argstr job "stdlib"
61+
- if: steps.stepCheck.outputs.status == 'built'
62+
name: Building/fetching current CI target
63+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
64+
--argstr job "bignums"
265
coq:
366
needs: []
467
runs-on: ubuntu-latest
@@ -115,6 +178,84 @@ jobs:
115178
name: Building/fetching current CI target
116179
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
117180
--argstr job "coq-elpi"
181+
coqeal:
182+
needs:
183+
- coq
184+
- mathcomp-algebra
185+
- bignums
186+
- multinomials
187+
- mathcomp-real-closed
188+
runs-on: ubuntu-latest
189+
steps:
190+
- name: Determine which commit to initially checkout
191+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
192+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
193+
}}\" >> $GITHUB_ENV\nfi\n"
194+
- name: Git checkout
195+
uses: actions/checkout@v4
196+
with:
197+
fetch-depth: 0
198+
ref: ${{ env.target_commit }}
199+
- name: Determine which commit to test
200+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
201+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
202+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
203+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
204+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
205+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
206+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
207+
\ fi\nfi\n"
208+
- name: Git checkout
209+
uses: actions/checkout@v4
210+
with:
211+
fetch-depth: 0
212+
ref: ${{ env.tested_commit }}
213+
- name: Cachix install
214+
uses: cachix/install-nix-action@v30
215+
with:
216+
nix_path: nixpkgs=channel:nixpkgs-unstable
217+
- name: Cachix setup coq-elpi
218+
uses: cachix/cachix-action@v15
219+
with:
220+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
221+
extraPullNames: coq, coq-community, math-comp
222+
name: coq-elpi
223+
- id: stepGetDerivation
224+
name: Getting derivation for current job (coqeal)
225+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
226+
\"coq-master\" --argstr job \"coqeal\" \\\n --dry-run 2> err > out || (touch
227+
fail; true)\n"
228+
- name: Error reporting
229+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
230+
- name: Failure check
231+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
232+
- id: stepCheck
233+
name: Checking presence of CI target for current job
234+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
235+
- if: steps.stepCheck.outputs.status == 'built'
236+
name: 'Building/fetching previous CI target: coq'
237+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
238+
--argstr job "coq"
239+
- if: steps.stepCheck.outputs.status == 'built'
240+
name: 'Building/fetching previous CI target: mathcomp-algebra'
241+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
242+
--argstr job "mathcomp-algebra"
243+
- if: steps.stepCheck.outputs.status == 'built'
244+
name: 'Building/fetching previous CI target: bignums'
245+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
246+
--argstr job "bignums"
247+
- if: steps.stepCheck.outputs.status == 'built'
248+
name: 'Building/fetching previous CI target: multinomials'
249+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
250+
--argstr job "multinomials"
251+
- if: steps.stepCheck.outputs.status == 'built'
252+
name: 'Building/fetching previous CI target: mathcomp-real-closed'
253+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
254+
--argstr job "mathcomp-real-closed"
255+
- if: steps.stepCheck.outputs.status == 'built'
256+
name: Building/fetching current CI target
257+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
258+
--argstr job "coqeal"
118259
hierarchy-builder:
119260
needs:
120261
- coq

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -248,6 +248,83 @@ jobs:
248248
name: Building/fetching current CI target
249249
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
250250
--argstr job "coq-elpi"
251+
coqeal:
252+
needs:
253+
- coq
254+
- mathcomp-algebra
255+
- multinomials
256+
- mathcomp-real-closed
257+
runs-on: ubuntu-latest
258+
steps:
259+
- name: Determine which commit to initially checkout
260+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
261+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
262+
}}\" >> $GITHUB_ENV\nfi\n"
263+
- name: Git checkout
264+
uses: actions/checkout@v4
265+
with:
266+
fetch-depth: 0
267+
ref: ${{ env.target_commit }}
268+
- name: Determine which commit to test
269+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
270+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
271+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
272+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
273+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
274+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
275+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
276+
\ fi\nfi\n"
277+
- name: Git checkout
278+
uses: actions/checkout@v4
279+
with:
280+
fetch-depth: 0
281+
ref: ${{ env.tested_commit }}
282+
- name: Cachix install
283+
uses: cachix/install-nix-action@v30
284+
with:
285+
nix_path: nixpkgs=channel:nixpkgs-unstable
286+
- name: Cachix setup coq-elpi
287+
uses: cachix/cachix-action@v15
288+
with:
289+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
290+
extraPullNames: coq, coq-community, math-comp
291+
name: coq-elpi
292+
- id: stepGetDerivation
293+
name: Getting derivation for current job (coqeal)
294+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
295+
\"rocq-9.0\" --argstr job \"coqeal\" \\\n --dry-run 2> err > out || (touch
296+
fail; true)\n"
297+
- name: Error reporting
298+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
299+
- name: Failure check
300+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
301+
- id: stepCheck
302+
name: Checking presence of CI target for current job
303+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
304+
- if: steps.stepCheck.outputs.status == 'built'
305+
name: 'Building/fetching previous CI target: coq'
306+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
307+
--argstr job "coq"
308+
- if: steps.stepCheck.outputs.status == 'built'
309+
name: 'Building/fetching previous CI target: mathcomp-algebra'
310+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
311+
--argstr job "mathcomp-algebra"
312+
- if: steps.stepCheck.outputs.status == 'built'
313+
name: 'Building/fetching previous CI target: bignums'
314+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
315+
--argstr job "bignums"
316+
- if: steps.stepCheck.outputs.status == 'built'
317+
name: 'Building/fetching previous CI target: multinomials'
318+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
319+
--argstr job "multinomials"
320+
- if: steps.stepCheck.outputs.status == 'built'
321+
name: 'Building/fetching previous CI target: mathcomp-real-closed'
322+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
323+
--argstr job "mathcomp-real-closed"
324+
- if: steps.stepCheck.outputs.status == 'built'
325+
name: Building/fetching current CI target
326+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "rocq-9.0"
327+
--argstr job "coqeal"
251328
hierarchy-builder:
252329
needs:
253330
- coq

‎.nix/config.nix

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -17,7 +17,6 @@ let master = [
1717
mathcomp-single-planB-src.job = false;
1818
mathcomp-single-planB.job = false;
1919
mathcomp-single.job = false;
20-
coqeal.job = false; # broken in master, c.f. https://github.com/coq/coq/pull/19228
2120

2221
deriving.job = false;
2322
reglang.job = false;
@@ -42,6 +41,7 @@ let master = [
4241
coq.override.version = "master";
4342
coq-elpi.override.elpi-version = "2.0.7";
4443
stdlib.override.version = "master";
44+
bignums.override.version = "master";
4545
};
4646

4747
/* uncomment bundle below if min and max elpi version start to differ

‎.nix/coq-nix-toolbox.nix

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"513125b0f59fa52c3919c5f2bdc63077d341b18a"
1+
"d914139ccc501c967eb97ea995f9765f4094d228"

0 commit comments

Comments
 (0)