Skip to content

Commit fc9741b

Browse files
proux01proux01
authored
Merge pull request #508 from proux01/ci-coqeal
[CI] Readd coqeal
2 parents a48844f + 52a031d commit fc9741b

File tree

5 files changed

+370
-4
lines changed

5 files changed

+370
-4
lines changed

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

Lines changed: 81 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -311,6 +311,87 @@ jobs:
311311
name: Building/fetching current CI target
312312
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
313313
--argstr job "coq-elpi"
314+
coqeal:
315+
needs:
316+
- coq
317+
- mathcomp-algebra
318+
- multinomials
319+
- mathcomp-real-closed
320+
runs-on: ubuntu-latest
321+
steps:
322+
- name: Determine which commit to initially checkout
323+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
324+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
325+
}}\" >> $GITHUB_ENV\nfi\n"
326+
- name: Git checkout
327+
uses: actions/checkout@v4
328+
with:
329+
fetch-depth: 0
330+
ref: ${{ env.target_commit }}
331+
- name: Determine which commit to test
332+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
333+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
334+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
335+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
336+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
337+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
338+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
339+
\ fi\nfi\n"
340+
- name: Git checkout
341+
uses: actions/checkout@v4
342+
with:
343+
fetch-depth: 0
344+
ref: ${{ env.tested_commit }}
345+
- name: Cachix install
346+
uses: cachix/install-nix-action@v30
347+
with:
348+
nix_path: nixpkgs=channel:nixpkgs-unstable
349+
- name: Cachix setup math-comp
350+
uses: cachix/cachix-action@v15
351+
with:
352+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
353+
extraPullNames: coq, coq-community
354+
name: math-comp
355+
- id: stepGetDerivation
356+
name: Getting derivation for current job (coqeal)
357+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
358+
\"coq-8.20\" --argstr job \"coqeal\" \\\n --dry-run 2> err > out || (touch
359+
fail; true)\n"
360+
- name: Error reporting
361+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
362+
- name: Failure check
363+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
364+
- id: stepCheck
365+
name: Checking presence of CI target for current job
366+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
367+
- if: steps.stepCheck.outputs.status == 'built'
368+
name: 'Building/fetching previous CI target: coq'
369+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
370+
--argstr job "coq"
371+
- if: steps.stepCheck.outputs.status == 'built'
372+
name: 'Building/fetching previous CI target: mathcomp-algebra'
373+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
374+
--argstr job "mathcomp-algebra"
375+
- if: steps.stepCheck.outputs.status == 'built'
376+
name: 'Building/fetching previous CI target: bignums'
377+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
378+
--argstr job "bignums"
379+
- if: steps.stepCheck.outputs.status == 'built'
380+
name: 'Building/fetching previous CI target: paramcoq'
381+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
382+
--argstr job "paramcoq"
383+
- if: steps.stepCheck.outputs.status == 'built'
384+
name: 'Building/fetching previous CI target: multinomials'
385+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
386+
--argstr job "multinomials"
387+
- if: steps.stepCheck.outputs.status == 'built'
388+
name: 'Building/fetching previous CI target: mathcomp-real-closed'
389+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
390+
--argstr job "mathcomp-real-closed"
391+
- if: steps.stepCheck.outputs.status == 'built'
392+
name: Building/fetching current CI target
393+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
394+
--argstr job "coqeal"
314395
coquelicot:
315396
needs:
316397
- coq

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

Lines changed: 77 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -311,6 +311,83 @@ jobs:
311311
name: Building/fetching current CI target
312312
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0"
313313
--argstr job "coq-elpi"
314+
coqeal:
315+
needs:
316+
- coq
317+
- mathcomp-algebra
318+
- multinomials
319+
- mathcomp-real-closed
320+
runs-on: ubuntu-latest
321+
steps:
322+
- name: Determine which commit to initially checkout
323+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
324+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
325+
}}\" >> $GITHUB_ENV\nfi\n"
326+
- name: Git checkout
327+
uses: actions/checkout@v4
328+
with:
329+
fetch-depth: 0
330+
ref: ${{ env.target_commit }}
331+
- name: Determine which commit to test
332+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
333+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
334+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
335+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
336+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
337+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
338+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
339+
\ fi\nfi\n"
340+
- name: Git checkout
341+
uses: actions/checkout@v4
342+
with:
343+
fetch-depth: 0
344+
ref: ${{ env.tested_commit }}
345+
- name: Cachix install
346+
uses: cachix/install-nix-action@v30
347+
with:
348+
nix_path: nixpkgs=channel:nixpkgs-unstable
349+
- name: Cachix setup math-comp
350+
uses: cachix/cachix-action@v15
351+
with:
352+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
353+
extraPullNames: coq, coq-community
354+
name: math-comp
355+
- id: stepGetDerivation
356+
name: Getting derivation for current job (coqeal)
357+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
358+
\"coq-9.0\" --argstr job \"coqeal\" \\\n --dry-run 2> err > out || (touch
359+
fail; true)\n"
360+
- name: Error reporting
361+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
362+
- name: Failure check
363+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
364+
- id: stepCheck
365+
name: Checking presence of CI target for current job
366+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
367+
- if: steps.stepCheck.outputs.status == 'built'
368+
name: 'Building/fetching previous CI target: coq'
369+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0"
370+
--argstr job "coq"
371+
- if: steps.stepCheck.outputs.status == 'built'
372+
name: 'Building/fetching previous CI target: mathcomp-algebra'
373+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0"
374+
--argstr job "mathcomp-algebra"
375+
- if: steps.stepCheck.outputs.status == 'built'
376+
name: 'Building/fetching previous CI target: bignums'
377+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0"
378+
--argstr job "bignums"
379+
- if: steps.stepCheck.outputs.status == 'built'
380+
name: 'Building/fetching previous CI target: multinomials'
381+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0"
382+
--argstr job "multinomials"
383+
- if: steps.stepCheck.outputs.status == 'built'
384+
name: 'Building/fetching previous CI target: mathcomp-real-closed'
385+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0"
386+
--argstr job "mathcomp-real-closed"
387+
- if: steps.stepCheck.outputs.status == 'built'
388+
name: Building/fetching current CI target
389+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-9.0"
390+
--argstr job "coqeal"
314391
deriving:
315392
needs:
316393
- coq

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

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

‎.nix/config.nix‎

Lines changed: 5 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -19,8 +19,7 @@
1919
mathcomp-bigenough.override.version = "master";
2020
multinomials.override.version = "master";
2121
mathcomp-real-closed.override.version = "master";
22-
# coqeal.override.version = "master";
23-
coqeal.job = false; # broken in master, c.f. https://github.com/coq/coq/pull/19228
22+
coqeal.override.version = "master";
2423
};
2524
in {
2625
"coq-master".coqPackages = mcHBcommon // {
@@ -34,24 +33,26 @@
3433

3534
"coq-9.0".coqPackages = mcHBcommon // {
3635
coq.override.version = "9.0";
37-
coq-elpi.override.version = "v2.4.0";
36+
coq-elpi.override.version = "master";
3837
coq-elpi.override.elpi-version = "2.0.7";
3938
};
4039

4140
"coq-8.20".coqPackages = mcHBcommon // {
4241
coq.override.version = "8.20";
43-
coq-elpi.override.version = "v2.4.0";
42+
coq-elpi.override.version = "master";
4443
coq-elpi.override.elpi-version = "2.0.7";
4544
};
4645

4746
"coq-8.19".coqPackages = mcHBcommon // {
4847
coq.override.version = "8.19";
48+
coqeal.job = false; # requries Coq >= 8.20 through coq-elpi master
4949
};
5050

5151
"coq-8.18".coqPackages = mcHBcommon // {
5252
coq.override.version = "8.18";
5353
mathcomp-classical.job = false; # Analysis master dropped suppor for 8.18
5454
mathcomp-analysis.job = false;
55+
coqeal.job = false; # requries Coq >= 8.20 through coq-elpi master
5556
};
5657

5758
};

0 commit comments

Comments
 (0)