Skip to content

Commit 508a7f4

Browse files
proux01proux01
committed
[CI] Add Coq 8.19
1 parent 5b6a147 commit 508a7f4

File tree

7 files changed

+1602
-54
lines changed

7 files changed

+1602
-54
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: 117 additions & 38 deletions
Original file line numberDiff line numberDiff line change
@@ -361,9 +361,12 @@ jobs:
361361
name: Building/fetching current CI target
362362
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
363363
--argstr job "coq-bits"
364-
coq-elpi:
364+
coqeal:
365365
needs:
366366
- coq
367+
- mathcomp-algebra
368+
- multinomials
369+
- mathcomp-real-closed
367370
runs-on: ubuntu-latest
368371
steps:
369372
- name: Determine which commit to initially checkout
@@ -400,25 +403,43 @@ jobs:
400403
extraPullNames: coq, coq-community
401404
name: math-comp
402405
- id: stepCheck
403-
name: Checking presence of CI target coq-elpi
406+
name: Checking presence of CI target coqeal
404407
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
405-
\ 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\
406409
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
407410
s/.*/built/\") >> $GITHUB_OUTPUT\n"
408411
- if: steps.stepCheck.outputs.status == 'built'
409412
name: 'Building/fetching previous CI target: coq'
410413
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
411414
--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"
412435
- if: steps.stepCheck.outputs.status == 'built'
413436
name: Building/fetching current CI target
414437
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
415-
--argstr job "coq-elpi"
416-
coqeal:
438+
--argstr job "coqeal"
439+
coquelicot:
417440
needs:
418441
- coq
419-
- mathcomp-algebra
420-
- multinomials
421-
- mathcomp-real-closed
442+
- mathcomp-ssreflect
422443
runs-on: ubuntu-latest
423444
steps:
424445
- name: Determine which commit to initially checkout
@@ -455,40 +476,24 @@ jobs:
455476
extraPullNames: coq, coq-community
456477
name: math-comp
457478
- id: stepCheck
458-
name: Checking presence of CI target coqeal
479+
name: Checking presence of CI target coquelicot
459480
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
460-
\ bundle \"coq-8.18\" --argstr job \"coqeal\" \\\n --dry-run 2>&1 > /dev/null)\n\
461-
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
462-
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"
463484
- if: steps.stepCheck.outputs.status == 'built'
464485
name: 'Building/fetching previous CI target: coq'
465486
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
466487
--argstr job "coq"
467488
- if: steps.stepCheck.outputs.status == 'built'
468-
name: 'Building/fetching previous CI target: mathcomp-algebra'
469-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
470-
--argstr job "mathcomp-algebra"
471-
- if: steps.stepCheck.outputs.status == 'built'
472-
name: 'Building/fetching previous CI target: bignums'
473-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
474-
--argstr job "bignums"
475-
- if: steps.stepCheck.outputs.status == 'built'
476-
name: 'Building/fetching previous CI target: paramcoq'
477-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
478-
--argstr job "paramcoq"
479-
- if: steps.stepCheck.outputs.status == 'built'
480-
name: 'Building/fetching previous CI target: multinomials'
481-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
482-
--argstr job "multinomials"
483-
- if: steps.stepCheck.outputs.status == 'built'
484-
name: 'Building/fetching previous CI target: mathcomp-real-closed'
489+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
485490
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
486-
--argstr job "mathcomp-real-closed"
491+
--argstr job "mathcomp-ssreflect"
487492
- if: steps.stepCheck.outputs.status == 'built'
488493
name: Building/fetching current CI target
489494
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
490-
--argstr job "coqeal"
491-
coquelicot:
495+
--argstr job "coquelicot"
496+
deriving:
492497
needs:
493498
- coq
494499
- mathcomp-ssreflect
@@ -528,11 +533,11 @@ jobs:
528533
extraPullNames: coq, coq-community
529534
name: math-comp
530535
- id: stepCheck
531-
name: Checking presence of CI target coquelicot
536+
name: Checking presence of CI target deriving
532537
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
533-
\ bundle \"coq-8.18\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1 >\
534-
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
535-
\ | 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"
536541
- if: steps.stepCheck.outputs.status == 'built'
537542
name: 'Building/fetching previous CI target: coq'
538543
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
@@ -544,7 +549,7 @@ jobs:
544549
- if: steps.stepCheck.outputs.status == 'built'
545550
name: Building/fetching current CI target
546551
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
547-
--argstr job "coquelicot"
552+
--argstr job "deriving"
548553
fourcolor:
549554
needs:
550555
- coq
@@ -615,7 +620,6 @@ jobs:
615620
hierarchy-builder:
616621
needs:
617622
- coq
618-
- coq-elpi
619623
runs-on: ubuntu-latest
620624
steps:
621625
- name: Determine which commit to initially checkout
@@ -669,6 +673,81 @@ jobs:
669673
name: Building/fetching current CI target
670674
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.18"
671675
--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"
672751
mathcomp:
673752
needs:
674753
- coq

0 commit comments

Comments
 (0)