Skip to content

Commit ae6bc33

Browse files
proux01proux01
committed
[CI] Add Coq 8.18
1 parent 9fb5b3e commit ae6bc33

File tree

7 files changed

+1837
-296
lines changed

7 files changed

+1837
-296
lines changed

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

Lines changed: 22 additions & 163 deletions
Original file line numberDiff line numberDiff line change
@@ -40,8 +40,8 @@ jobs:
4040
name: Checking presence of CI target coq
4141
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
4242
\ bundle \"coq-8.15\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
43-
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
44-
\ \"built:\" | sed \"s/.*/built/\")\n"
43+
echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\
44+
\ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
4545
- if: steps.stepCheck.outputs.status == 'built'
4646
name: Building/fetching current CI target
4747
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -88,8 +88,8 @@ jobs:
8888
name: Checking presence of CI target coq-bits
8989
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
9090
\ bundle \"coq-8.15\" --argstr job \"coq-bits\" \\\n --dry-run 2>&1 > /dev/null)\n\
91-
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
92-
\ \"built:\" | sed \"s/.*/built/\")\n"
91+
echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\
92+
\ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
9393
- if: steps.stepCheck.outputs.status == 'built'
9494
name: 'Building/fetching previous CI target: coq'
9595
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -144,8 +144,8 @@ jobs:
144144
name: Checking presence of CI target fourcolor
145145
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
146146
\ bundle \"coq-8.15\" --argstr job \"fourcolor\" \\\n --dry-run 2>&1 > /dev/null)\n\
147-
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
148-
\ \"built:\" | sed \"s/.*/built/\")\n"
147+
echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\
148+
\ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
149149
- if: steps.stepCheck.outputs.status == 'built'
150150
name: 'Building/fetching previous CI target: coq'
151151
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -208,8 +208,8 @@ jobs:
208208
name: Checking presence of CI target hierarchy-builder
209209
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
210210
\ bundle \"coq-8.15\" --argstr job \"hierarchy-builder\" \\\n --dry-run\
211-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
212-
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
211+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\
212+
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
213213
- if: steps.stepCheck.outputs.status == 'built'
214214
name: 'Building/fetching previous CI target: coq'
215215
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -264,8 +264,8 @@ jobs:
264264
name: Checking presence of CI target hierarchy-builder-shim
265265
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
266266
\ bundle \"coq-8.15\" --argstr job \"hierarchy-builder-shim\" \\\n --dry-run\
267-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
268-
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
267+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\
268+
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
269269
- if: steps.stepCheck.outputs.status == 'built'
270270
name: 'Building/fetching previous CI target: coq'
271271
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -320,8 +320,8 @@ jobs:
320320
name: Checking presence of CI target interval
321321
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
322322
\ bundle \"coq-8.15\" --argstr job \"interval\" \\\n --dry-run 2>&1 > /dev/null)\n\
323-
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
324-
\ \"built:\" | sed \"s/.*/built/\")\n"
323+
echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\
324+
\ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
325325
- if: steps.stepCheck.outputs.status == 'built'
326326
name: 'Building/fetching previous CI target: coq'
327327
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -350,147 +350,6 @@ jobs:
350350
name: Building/fetching current CI target
351351
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
352352
--argstr job "interval"
353-
mathcomp-analysis:
354-
needs:
355-
- coq
356-
- mathcomp-classical
357-
- hierarchy-builder
358-
runs-on: ubuntu-latest
359-
steps:
360-
- name: Determine which commit to initially checkout
361-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
362-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
363-
\ }}\" >> $GITHUB_ENV\nfi\n"
364-
- name: Git checkout
365-
uses: actions/checkout@v3
366-
with:
367-
fetch-depth: 0
368-
ref: ${{ env.target_commit }}
369-
- name: Determine which commit to test
370-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
371-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
372-
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
373-
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
374-
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
375-
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
376-
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
377-
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
378-
- name: Git checkout
379-
uses: actions/checkout@v3
380-
with:
381-
fetch-depth: 0
382-
ref: ${{ env.tested_commit }}
383-
- name: Cachix install
384-
uses: cachix/install-nix-action@v20
385-
with:
386-
nix_path: nixpkgs=channel:nixpkgs-unstable
387-
- name: Cachix setup math-comp
388-
uses: cachix/cachix-action@v12
389-
with:
390-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
391-
extraPullNames: coq, coq-community
392-
name: math-comp
393-
- id: stepCheck
394-
name: Checking presence of CI target mathcomp-analysis
395-
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
396-
\ bundle \"coq-8.15\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\
397-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
398-
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
399-
- if: steps.stepCheck.outputs.status == 'built'
400-
name: 'Building/fetching previous CI target: coq'
401-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
402-
--argstr job "coq"
403-
- if: steps.stepCheck.outputs.status == 'built'
404-
name: 'Building/fetching previous CI target: mathcomp-classical'
405-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
406-
--argstr job "mathcomp-classical"
407-
- if: steps.stepCheck.outputs.status == 'built'
408-
name: 'Building/fetching previous CI target: mathcomp-field'
409-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
410-
--argstr job "mathcomp-field"
411-
- if: steps.stepCheck.outputs.status == 'built'
412-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
413-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
414-
--argstr job "mathcomp-bigenough"
415-
- if: steps.stepCheck.outputs.status == 'built'
416-
name: 'Building/fetching previous CI target: hierarchy-builder'
417-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
418-
--argstr job "hierarchy-builder"
419-
- if: steps.stepCheck.outputs.status == 'built'
420-
name: Building/fetching current CI target
421-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
422-
--argstr job "mathcomp-analysis"
423-
mathcomp-classical:
424-
needs:
425-
- coq
426-
- mathcomp-finmap
427-
- hierarchy-builder
428-
- hierarchy-builder
429-
runs-on: ubuntu-latest
430-
steps:
431-
- name: Determine which commit to initially checkout
432-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
433-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
434-
\ }}\" >> $GITHUB_ENV\nfi\n"
435-
- name: Git checkout
436-
uses: actions/checkout@v3
437-
with:
438-
fetch-depth: 0
439-
ref: ${{ env.target_commit }}
440-
- name: Determine which commit to test
441-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
442-
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
443-
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
444-
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
445-
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
446-
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
447-
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
448-
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
449-
- name: Git checkout
450-
uses: actions/checkout@v3
451-
with:
452-
fetch-depth: 0
453-
ref: ${{ env.tested_commit }}
454-
- name: Cachix install
455-
uses: cachix/install-nix-action@v20
456-
with:
457-
nix_path: nixpkgs=channel:nixpkgs-unstable
458-
- name: Cachix setup math-comp
459-
uses: cachix/cachix-action@v12
460-
with:
461-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
462-
extraPullNames: coq, coq-community
463-
name: math-comp
464-
- id: stepCheck
465-
name: Checking presence of CI target mathcomp-classical
466-
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
467-
\ bundle \"coq-8.15\" --argstr job \"mathcomp-classical\" \\\n --dry-run\
468-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
469-
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
470-
- if: steps.stepCheck.outputs.status == 'built'
471-
name: 'Building/fetching previous CI target: coq'
472-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
473-
--argstr job "coq"
474-
- if: steps.stepCheck.outputs.status == 'built'
475-
name: 'Building/fetching previous CI target: mathcomp-algebra'
476-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
477-
--argstr job "mathcomp-algebra"
478-
- if: steps.stepCheck.outputs.status == 'built'
479-
name: 'Building/fetching previous CI target: mathcomp-finmap'
480-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
481-
--argstr job "mathcomp-finmap"
482-
- if: steps.stepCheck.outputs.status == 'built'
483-
name: 'Building/fetching previous CI target: hierarchy-builder'
484-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
485-
--argstr job "hierarchy-builder"
486-
- if: steps.stepCheck.outputs.status == 'built'
487-
name: 'Building/fetching previous CI target: hierarchy-builder'
488-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
489-
--argstr job "hierarchy-builder"
490-
- if: steps.stepCheck.outputs.status == 'built'
491-
name: Building/fetching current CI target
492-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
493-
--argstr job "mathcomp-classical"
494353
mathcomp-finmap:
495354
needs:
496355
- coq
@@ -533,8 +392,8 @@ jobs:
533392
name: Checking presence of CI target mathcomp-finmap
534393
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
535394
\ bundle \"coq-8.15\" --argstr job \"mathcomp-finmap\" \\\n --dry-run 2>&1\
536-
\ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\
537-
\ | grep \"built:\" | sed \"s/.*/built/\")\n"
395+
\ > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep\
396+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
538397
- if: steps.stepCheck.outputs.status == 'built'
539398
name: 'Building/fetching previous CI target: coq'
540399
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -589,8 +448,8 @@ jobs:
589448
name: Checking presence of CI target mathcomp-single
590449
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
591450
\ bundle \"coq-8.15\" --argstr job \"mathcomp-single\" \\\n --dry-run 2>&1\
592-
\ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\
593-
\ | grep \"built:\" | sed \"s/.*/built/\")\n"
451+
\ > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep\
452+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
594453
- if: steps.stepCheck.outputs.status == 'built'
595454
name: 'Building/fetching previous CI target: coq'
596455
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -642,8 +501,8 @@ jobs:
642501
name: Checking presence of CI target mathcomp-single-planB-src
643502
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
644503
\ bundle \"coq-8.15\" --argstr job \"mathcomp-single-planB-src\" \\\n --dry-run\
645-
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
646-
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
504+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho name=status::$(echo $nb_dry_run\
505+
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
647506
- if: steps.stepCheck.outputs.status == 'built'
648507
name: 'Building/fetching previous CI target: coq'
649508
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -702,8 +561,8 @@ jobs:
702561
name: Checking presence of CI target odd-order
703562
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
704563
\ bundle \"coq-8.15\" --argstr job \"odd-order\" \\\n --dry-run 2>&1 > /dev/null)\n\
705-
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
706-
\ \"built:\" | sed \"s/.*/built/\")\n"
564+
echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\
565+
\ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
707566
- if: steps.stepCheck.outputs.status == 'built'
708567
name: 'Building/fetching previous CI target: coq'
709568
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
@@ -782,8 +641,8 @@ jobs:
782641
name: Checking presence of CI target reglang
783642
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
784643
\ bundle \"coq-8.15\" --argstr job \"reglang\" \\\n --dry-run 2>&1 > /dev/null)\n\
785-
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
786-
\ \"built:\" | sed \"s/.*/built/\")\n"
644+
echo $nb_dry_run\necho name=status::$(echo $nb_dry_run | grep \"built:\" |\
645+
\ sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
787646
- if: steps.stepCheck.outputs.status == 'built'
788647
name: 'Building/fetching previous CI target: coq'
789648
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"

0 commit comments

Comments
 (0)