Skip to content

Commit 494dd62

Browse files
CohenCyrilCohenCyril
authored
Merge pull request #409 from proux01/ci_coq819
[CI] Add Coq 8.19
2 parents 5978ba7 + 508a7f4 commit 494dd62

File tree

10 files changed

+1597
-157
lines changed

10 files changed

+1597
-157
lines changed

‎.github/workflows/main.yml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -18,9 +18,8 @@ jobs:
1818
fail-fast: false
1919
matrix:
2020
coq_version:
21-
- '8.16'
22-
- '8.17'
2321
- '8.18'
22+
- '8.19'
2423
steps:
2524
- uses: actions/checkout@v2
2625
- uses: coq-community/docker-coq-action@v1

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

Lines changed: 182 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,69 @@
11
jobs:
2+
QuickChick:
3+
needs:
4+
- coq
5+
- mathcomp-ssreflect
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@v3
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 ${{\
20+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
21+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
22+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
23+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
24+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
25+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
26+
- name: Git checkout
27+
uses: actions/checkout@v3
28+
with:
29+
fetch-depth: 0
30+
ref: ${{ env.tested_commit }}
31+
- name: Cachix install
32+
uses: cachix/install-nix-action@v20
33+
with:
34+
nix_path: nixpkgs=channel:nixpkgs-unstable
35+
- name: Cachix setup math-comp
36+
uses: cachix/cachix-action@v12
37+
with:
38+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
39+
extraPullNames: coq, coq-community
40+
name: math-comp
41+
- id: stepCheck
42+
name: Checking presence of CI target QuickChick
43+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
44+
\ bundle \"coq-8.18\" --argstr job \"QuickChick\" \\\n --dry-run 2>&1 >\
45+
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
46+
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
47+
- if: steps.stepCheck.outputs.status == 'built'
48+
name: 'Building/fetching previous CI target: coq'
49+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
50+
--argstr job "coq"
51+
- if: steps.stepCheck.outputs.status == 'built'
52+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
53+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
54+
--argstr job "mathcomp-ssreflect"
55+
- if: steps.stepCheck.outputs.status == 'built'
56+
name: 'Building/fetching previous CI target: coq-ext-lib'
57+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
58+
--argstr job "coq-ext-lib"
59+
- if: steps.stepCheck.outputs.status == 'built'
60+
name: 'Building/fetching previous CI target: simple-io'
61+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
62+
--argstr job "simple-io"
63+
- if: steps.stepCheck.outputs.status == 'built'
64+
name: Building/fetching current CI target
65+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
66+
--argstr job "QuickChick"
267
Verdi:
368
needs:
469
- coq
@@ -296,9 +361,12 @@ jobs:
296361
name: Building/fetching current CI target
297362
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
298363
--argstr job "coq-bits"
299-
coq-elpi:
364+
coqeal:
300365
needs:
301366
- coq
367+
- mathcomp-algebra
368+
- multinomials
369+
- mathcomp-real-closed
302370
runs-on: ubuntu-latest
303371
steps:
304372
- name: Determine which commit to initially checkout
@@ -335,25 +403,43 @@ jobs:
335403
extraPullNames: coq, coq-community
336404
name: math-comp
337405
- id: stepCheck
338-
name: Checking presence of CI target coq-elpi
406+
name: Checking presence of CI target coqeal
339407
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
340-
\ bundle \"coq-8.18\" --argstr job \"coq-elpi\" \\\n --dry-run 2>&1 > /dev/null)\n\
408+
\ bundle \"coq-8.18\" --argstr job \"coqeal\" \\\n --dry-run 2>&1 > /dev/null)\n\
341409
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
342410
s/.*/built/\") >> $GITHUB_OUTPUT\n"
343411
- if: steps.stepCheck.outputs.status == 'built'
344412
name: 'Building/fetching previous CI target: coq'
345413
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
346414
--argstr job "coq"
415+
- if: steps.stepCheck.outputs.status == 'built'
416+
name: 'Building/fetching previous CI target: mathcomp-algebra'
417+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
418+
--argstr job "mathcomp-algebra"
419+
- if: steps.stepCheck.outputs.status == 'built'
420+
name: 'Building/fetching previous CI target: bignums'
421+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
422+
--argstr job "bignums"
423+
- if: steps.stepCheck.outputs.status == 'built'
424+
name: 'Building/fetching previous CI target: paramcoq'
425+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
426+
--argstr job "paramcoq"
427+
- if: steps.stepCheck.outputs.status == 'built'
428+
name: 'Building/fetching previous CI target: multinomials'
429+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
430+
--argstr job "multinomials"
431+
- if: steps.stepCheck.outputs.status == 'built'
432+
name: 'Building/fetching previous CI target: mathcomp-real-closed'
433+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
434+
--argstr job "mathcomp-real-closed"
347435
- if: steps.stepCheck.outputs.status == 'built'
348436
name: Building/fetching current CI target
349437
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
350-
--argstr job "coq-elpi"
351-
coqeal:
438+
--argstr job "coqeal"
439+
coquelicot:
352440
needs:
353441
- coq
354-
- mathcomp-algebra
355-
- multinomials
356-
- mathcomp-real-closed
442+
- mathcomp-ssreflect
357443
runs-on: ubuntu-latest
358444
steps:
359445
- name: Determine which commit to initially checkout
@@ -390,40 +476,24 @@ jobs:
390476
extraPullNames: coq, coq-community
391477
name: math-comp
392478
- id: stepCheck
393-
name: Checking presence of CI target coqeal
479+
name: Checking presence of CI target coquelicot
394480
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
395-
\ bundle \"coq-8.18\" --argstr job \"coqeal\" \\\n --dry-run 2>&1 > /dev/null)\n\
396-
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
397-
s/.*/built/\") >> $GITHUB_OUTPUT\n"
481+
\ bundle \"coq-8.18\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\
482+
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
483+
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
398484
- if: steps.stepCheck.outputs.status == 'built'
399485
name: 'Building/fetching previous CI target: coq'
400486
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
401487
--argstr job "coq"
402488
- if: steps.stepCheck.outputs.status == 'built'
403-
name: 'Building/fetching previous CI target: mathcomp-algebra'
404-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
405-
--argstr job "mathcomp-algebra"
406-
- if: steps.stepCheck.outputs.status == 'built'
407-
name: 'Building/fetching previous CI target: bignums'
408-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
409-
--argstr job "bignums"
410-
- if: steps.stepCheck.outputs.status == 'built'
411-
name: 'Building/fetching previous CI target: paramcoq'
412-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
413-
--argstr job "paramcoq"
414-
- if: steps.stepCheck.outputs.status == 'built'
415-
name: 'Building/fetching previous CI target: multinomials'
416-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
417-
--argstr job "multinomials"
418-
- if: steps.stepCheck.outputs.status == 'built'
419-
name: 'Building/fetching previous CI target: mathcomp-real-closed'
489+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
420490
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
421-
--argstr job "mathcomp-real-closed"
491+
--argstr job "mathcomp-ssreflect"
422492
- if: steps.stepCheck.outputs.status == 'built'
423493
name: Building/fetching current CI target
424494
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
425-
--argstr job "coqeal"
426-
coquelicot:
495+
--argstr job "coquelicot"
496+
deriving:
427497
needs:
428498
- coq
429499
- mathcomp-ssreflect
@@ -463,11 +533,11 @@ jobs:
463533
extraPullNames: coq, coq-community
464534
name: math-comp
465535
- id: stepCheck
466-
name: Checking presence of CI target coquelicot
536+
name: Checking presence of CI target deriving
467537
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
468-
\ bundle \"coq-8.18\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\
469-
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
470-
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
538+
\ bundle \"coq-8.18\" --argstr job \"deriving\" \\\n --dry-run 2>&1 > /dev/null)\n\
539+
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
540+
s/.*/built/\") >> $GITHUB_OUTPUT\n"
471541
- if: steps.stepCheck.outputs.status == 'built'
472542
name: 'Building/fetching previous CI target: coq'
473543
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
@@ -479,7 +549,7 @@ jobs:
479549
- if: steps.stepCheck.outputs.status == 'built'
480550
name: Building/fetching current CI target
481551
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
482-
--argstr job "coquelicot"
552+
--argstr job "deriving"
483553
fourcolor:
484554
needs:
485555
- coq
@@ -550,7 +620,6 @@ jobs:
550620
hierarchy-builder:
551621
needs:
552622
- coq
553-
- coq-elpi
554623
runs-on: ubuntu-latest
555624
steps:
556625
- name: Determine which commit to initially checkout
@@ -604,6 +673,81 @@ jobs:
604673
name: Building/fetching current CI target
605674
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
606675
--argstr job "hierarchy-builder"
676+
interval:
677+
needs:
678+
- coq
679+
- coquelicot
680+
- mathcomp-ssreflect
681+
- mathcomp-fingroup
682+
runs-on: ubuntu-latest
683+
steps:
684+
- name: Determine which commit to initially checkout
685+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
686+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
687+
\ }}\" >> $GITHUB_ENV\nfi\n"
688+
- name: Git checkout
689+
uses: actions/checkout@v3
690+
with:
691+
fetch-depth: 0
692+
ref: ${{ env.target_commit }}
693+
- name: Determine which commit to test
694+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
695+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
696+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
697+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
698+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
699+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
700+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
701+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
702+
- name: Git checkout
703+
uses: actions/checkout@v3
704+
with:
705+
fetch-depth: 0
706+
ref: ${{ env.tested_commit }}
707+
- name: Cachix install
708+
uses: cachix/install-nix-action@v20
709+
with:
710+
nix_path: nixpkgs=channel:nixpkgs-unstable
711+
- name: Cachix setup math-comp
712+
uses: cachix/cachix-action@v12
713+
with:
714+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
715+
extraPullNames: coq, coq-community
716+
name: math-comp
717+
- id: stepCheck
718+
name: Checking presence of CI target interval
719+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
720+
\ bundle \"coq-8.18\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\
721+
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
722+
s/.*/built/\") >> $GITHUB_OUTPUT\n"
723+
- if: steps.stepCheck.outputs.status == 'built'
724+
name: 'Building/fetching previous CI target: coq'
725+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
726+
--argstr job "coq"
727+
- if: steps.stepCheck.outputs.status == 'built'
728+
name: 'Building/fetching previous CI target: bignums'
729+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
730+
--argstr job "bignums"
731+
- if: steps.stepCheck.outputs.status == 'built'
732+
name: 'Building/fetching previous CI target: coquelicot'
733+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
734+
--argstr job "coquelicot"
735+
- if: steps.stepCheck.outputs.status == 'built'
736+
name: 'Building/fetching previous CI target: flocq'
737+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
738+
--argstr job "flocq"
739+
- if: steps.stepCheck.outputs.status == 'built'
740+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
741+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
742+
--argstr job "mathcomp-ssreflect"
743+
- if: steps.stepCheck.outputs.status == 'built'
744+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
745+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
746+
--argstr job "mathcomp-fingroup"
747+
- if: steps.stepCheck.outputs.status == 'built'
748+
name: Building/fetching current CI target
749+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
750+
--argstr job "interval"
607751
mathcomp:
608752
needs:
609753
- coq

0 commit comments

Comments
 (0)