Skip to content

Commit e902da5

Browse files
garesgares
authored
Merge pull request #685 from proux01/ci-coqeal
[CI] Add coqeal and Coq 8.20
2 parents d650983 + 47acf9d commit e902da5

File tree

7 files changed

+2227
-81
lines changed

7 files changed

+2227
-81
lines changed

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

Lines changed: 361 additions & 0 deletions
Large diffs are not rendered by default.

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

Lines changed: 1382 additions & 0 deletions
Large diffs are not rendered by default.

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

Lines changed: 226 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -98,6 +98,73 @@ jobs:
9898
name: Building/fetching current CI target
9999
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
100100
--argstr job "coq-elpi"
101+
coqeal:
102+
needs:
103+
- coq
104+
- mathcomp-algebra
105+
- multinomials
106+
- mathcomp-real-closed
107+
runs-on: ubuntu-latest
108+
steps:
109+
- name: Determine which commit to initially checkout
110+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
111+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
112+
\ }}\" >> $GITHUB_ENV\nfi\n"
113+
- name: Git checkout
114+
uses: actions/checkout@v4
115+
with:
116+
fetch-depth: 0
117+
ref: ${{ env.target_commit }}
118+
- name: Determine which commit to test
119+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
120+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
121+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
122+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
123+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
124+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
125+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
126+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
127+
- name: Git checkout
128+
uses: actions/checkout@v4
129+
with:
130+
fetch-depth: 0
131+
ref: ${{ env.tested_commit }}
132+
- name: Cachix install
133+
uses: cachix/install-nix-action@v27
134+
with:
135+
nix_path: nixpkgs=channel:nixpkgs-unstable
136+
- name: Cachix setup coq-elpi
137+
uses: cachix/cachix-action@v15
138+
with:
139+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
140+
extraPullNames: coq, coq-community, math-comp
141+
name: coq-elpi
142+
- id: stepCheck
143+
name: Checking presence of CI target coqeal
144+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
145+
\ bundle \"coq-master-min-elpi\" --argstr job \"coqeal\" \\\n --dry-run\
146+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
147+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
148+
- if: steps.stepCheck.outputs.status == 'built'
149+
name: 'Building/fetching previous CI target: coq'
150+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
151+
--argstr job "coq"
152+
- if: steps.stepCheck.outputs.status == 'built'
153+
name: 'Building/fetching previous CI target: mathcomp-algebra'
154+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
155+
--argstr job "mathcomp-algebra"
156+
- if: steps.stepCheck.outputs.status == 'built'
157+
name: 'Building/fetching previous CI target: multinomials'
158+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
159+
--argstr job "multinomials"
160+
- if: steps.stepCheck.outputs.status == 'built'
161+
name: 'Building/fetching previous CI target: mathcomp-real-closed'
162+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
163+
--argstr job "mathcomp-real-closed"
164+
- if: steps.stepCheck.outputs.status == 'built'
165+
name: Building/fetching current CI target
166+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
167+
--argstr job "coqeal"
101168
hierarchy-builder:
102169
needs:
103170
- coq
@@ -783,6 +850,88 @@ jobs:
783850
name: Building/fetching current CI target
784851
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
785852
--argstr job "mathcomp-finmap"
853+
mathcomp-real-closed:
854+
needs:
855+
- coq
856+
- mathcomp-ssreflect
857+
- mathcomp-algebra
858+
- mathcomp-field
859+
- mathcomp-fingroup
860+
- mathcomp-solvable
861+
- mathcomp-bigenough
862+
runs-on: ubuntu-latest
863+
steps:
864+
- name: Determine which commit to initially checkout
865+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
866+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
867+
\ }}\" >> $GITHUB_ENV\nfi\n"
868+
- name: Git checkout
869+
uses: actions/checkout@v4
870+
with:
871+
fetch-depth: 0
872+
ref: ${{ env.target_commit }}
873+
- name: Determine which commit to test
874+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
875+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
876+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
877+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
878+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
879+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
880+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
881+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
882+
- name: Git checkout
883+
uses: actions/checkout@v4
884+
with:
885+
fetch-depth: 0
886+
ref: ${{ env.tested_commit }}
887+
- name: Cachix install
888+
uses: cachix/install-nix-action@v27
889+
with:
890+
nix_path: nixpkgs=channel:nixpkgs-unstable
891+
- name: Cachix setup coq-elpi
892+
uses: cachix/cachix-action@v15
893+
with:
894+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
895+
extraPullNames: coq, coq-community, math-comp
896+
name: coq-elpi
897+
- id: stepCheck
898+
name: Checking presence of CI target mathcomp-real-closed
899+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
900+
\ bundle \"coq-master-min-elpi\" --argstr job \"mathcomp-real-closed\" \\\n\
901+
\ --dry-run 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run\
902+
\ | grep \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
903+
- if: steps.stepCheck.outputs.status == 'built'
904+
name: 'Building/fetching previous CI target: coq'
905+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
906+
--argstr job "coq"
907+
- if: steps.stepCheck.outputs.status == 'built'
908+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
909+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
910+
--argstr job "mathcomp-ssreflect"
911+
- if: steps.stepCheck.outputs.status == 'built'
912+
name: 'Building/fetching previous CI target: mathcomp-algebra'
913+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
914+
--argstr job "mathcomp-algebra"
915+
- if: steps.stepCheck.outputs.status == 'built'
916+
name: 'Building/fetching previous CI target: mathcomp-field'
917+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
918+
--argstr job "mathcomp-field"
919+
- if: steps.stepCheck.outputs.status == 'built'
920+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
921+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
922+
--argstr job "mathcomp-fingroup"
923+
- if: steps.stepCheck.outputs.status == 'built'
924+
name: 'Building/fetching previous CI target: mathcomp-solvable'
925+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
926+
--argstr job "mathcomp-solvable"
927+
- if: steps.stepCheck.outputs.status == 'built'
928+
name: 'Building/fetching previous CI target: mathcomp-bigenough'
929+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
930+
--argstr job "mathcomp-bigenough"
931+
- if: steps.stepCheck.outputs.status == 'built'
932+
name: Building/fetching current CI target
933+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
934+
--argstr job "mathcomp-real-closed"
786935
mathcomp-solvable:
787936
needs:
788937
- coq
@@ -912,6 +1061,83 @@ jobs:
9121061
name: Building/fetching current CI target
9131062
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
9141063
--argstr job "mathcomp-ssreflect"
1064+
multinomials:
1065+
needs:
1066+
- coq
1067+
- mathcomp-ssreflect
1068+
- mathcomp-algebra
1069+
- mathcomp-finmap
1070+
- mathcomp-fingroup
1071+
- mathcomp-bigenough
1072+
runs-on: ubuntu-latest
1073+
steps:
1074+
- name: Determine which commit to initially checkout
1075+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
1076+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
1077+
\ }}\" >> $GITHUB_ENV\nfi\n"
1078+
- name: Git checkout
1079+
uses: actions/checkout@v4
1080+
with:
1081+
fetch-depth: 0
1082+
ref: ${{ env.target_commit }}
1083+
- name: Determine which commit to test
1084+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
1085+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
1086+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
1087+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
1088+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
1089+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
1090+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
1091+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
1092+
- name: Git checkout
1093+
uses: actions/checkout@v4
1094+
with:
1095+
fetch-depth: 0
1096+
ref: ${{ env.tested_commit }}
1097+
- name: Cachix install
1098+
uses: cachix/install-nix-action@v27
1099+
with:
1100+
nix_path: nixpkgs=channel:nixpkgs-unstable
1101+
- name: Cachix setup coq-elpi
1102+
uses: cachix/cachix-action@v15
1103+
with:
1104+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1105+
extraPullNames: coq, coq-community, math-comp
1106+
name: coq-elpi
1107+
- id: stepCheck
1108+
name: Checking presence of CI target multinomials
1109+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1110+
\ bundle \"coq-master-min-elpi\" --argstr job \"multinomials\" \\\n --dry-run\
1111+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
1112+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
1113+
- if: steps.stepCheck.outputs.status == 'built'
1114+
name: 'Building/fetching previous CI target: coq'
1115+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
1116+
--argstr job "coq"
1117+
- if: steps.stepCheck.outputs.status == 'built'
1118+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
1119+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
1120+
--argstr job "mathcomp-ssreflect"
1121+
- if: steps.stepCheck.outputs.status == 'built'
1122+
name: 'Building/fetching previous CI target: mathcomp-algebra'
1123+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
1124+
--argstr job "mathcomp-algebra"
1125+
- if: steps.stepCheck.outputs.status == 'built'
1126+
name: 'Building/fetching previous CI target: mathcomp-finmap'
1127+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
1128+
--argstr job "mathcomp-finmap"
1129+
- if: steps.stepCheck.outputs.status == 'built'
1130+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
1131+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
1132+
--argstr job "mathcomp-fingroup"
1133+
- if: steps.stepCheck.outputs.status == 'built'
1134+
name: 'Building/fetching previous CI target: mathcomp-bigenough'
1135+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
1136+
--argstr job "mathcomp-bigenough"
1137+
- if: steps.stepCheck.outputs.status == 'built'
1138+
name: Building/fetching current CI target
1139+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master-min-elpi"
1140+
--argstr job "multinomials"
9151141
odd-order:
9161142
needs:
9171143
- coq

0 commit comments

Comments
 (0)