Skip to content

Commit 6ec7d0d

Browse files
4ever24ever2
authored
Merge pull request #91 from SSProve/coq-9.1
Support Rocq 9.1
2 parents c2e501a + 40217f0 commit 6ec7d0d

38 files changed

+665
-272
lines changed

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

Lines changed: 66 additions & 67 deletions
Original file line numberDiff line numberDiff line change
@@ -40,18 +40,19 @@ jobs:
4040
name: Getting derivation for current job (coq)
4141
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
4242
\"8.20\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail;
43-
true)\n"
44-
- name: Error reporting
45-
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
46-
- name: Failure check
47-
run: if [ -e fail ]; then exit 1; else exit 0; fi;
43+
true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
44+
failed\"; exit 1; fi\n"
4845
- id: stepCheck
4946
name: Checking presence of CI target for current job
50-
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
51-
- if: steps.stepCheck.outputs.status == 'built'
47+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
48+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
49+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
50+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
51+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
52+
- if: steps.stepCheck.outputs.status != 'fetched'
5253
name: Building/fetching current CI target
53-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
54-
job "coq"
54+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
55+
--argstr job "coq"
5556
mathcomp-analysis:
5657
needs:
5758
- coq
@@ -94,38 +95,35 @@ jobs:
9495
name: Getting derivation for current job (mathcomp-analysis)
9596
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
9697
\"8.20\" --argstr job \"mathcomp-analysis\" \\\n --dry-run 2> err > out
97-
|| (touch fail; true)\n"
98-
- name: Error reporting
99-
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
100-
- name: Failure check
101-
run: if [ -e fail ]; then exit 1; else exit 0; fi;
98+
|| (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting
99+
derivation failed\"; exit 1; fi\n"
102100
- id: stepCheck
103101
name: Checking presence of CI target for current job
104-
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
105-
- if: steps.stepCheck.outputs.status == 'built'
102+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
103+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
104+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
105+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
106+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
107+
- if: steps.stepCheck.outputs.status != 'fetched'
106108
name: 'Building/fetching previous CI target: coq'
107-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
108-
job "coq"
109-
- if: steps.stepCheck.outputs.status == 'built'
109+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
110+
--argstr job "coq"
111+
- if: steps.stepCheck.outputs.status != 'fetched'
110112
name: 'Building/fetching previous CI target: mathcomp-reals'
111-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
112-
job "mathcomp-reals"
113-
- if: steps.stepCheck.outputs.status == 'built'
113+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
114+
--argstr job "mathcomp-reals"
115+
- if: steps.stepCheck.outputs.status != 'fetched'
114116
name: 'Building/fetching previous CI target: mathcomp-field'
115-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
116-
job "mathcomp-field"
117-
- if: steps.stepCheck.outputs.status == 'built'
117+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
118+
--argstr job "mathcomp-field"
119+
- if: steps.stepCheck.outputs.status != 'fetched'
118120
name: 'Building/fetching previous CI target: mathcomp-bigenough'
119-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
120-
job "mathcomp-bigenough"
121-
- if: steps.stepCheck.outputs.status == 'built'
122-
name: 'Building/fetching previous CI target: hierarchy-builder'
123-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
124-
job "hierarchy-builder"
125-
- if: steps.stepCheck.outputs.status == 'built'
121+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
122+
--argstr job "mathcomp-bigenough"
123+
- if: steps.stepCheck.outputs.status != 'fetched'
126124
name: Building/fetching current CI target
127-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
128-
job "mathcomp-analysis"
125+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
126+
--argstr job "mathcomp-analysis"
129127
ssprove:
130128
needs:
131129
- coq
@@ -169,50 +167,51 @@ jobs:
169167
name: Getting derivation for current job (ssprove)
170168
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
171169
\"8.20\" --argstr job \"ssprove\" \\\n --dry-run 2> err > out || (touch
172-
fail; true)\n"
173-
- name: Error reporting
174-
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
175-
- name: Failure check
176-
run: if [ -e fail ]; then exit 1; else exit 0; fi;
170+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
171+
failed\"; exit 1; fi\n"
177172
- id: stepCheck
178173
name: Checking presence of CI target for current job
179-
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
180-
- if: steps.stepCheck.outputs.status == 'built'
174+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
175+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
176+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
177+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
178+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
179+
- if: steps.stepCheck.outputs.status != 'fetched'
181180
name: 'Building/fetching previous CI target: coq'
182-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
183-
job "coq"
184-
- if: steps.stepCheck.outputs.status == 'built'
181+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
182+
--argstr job "coq"
183+
- if: steps.stepCheck.outputs.status != 'fetched'
185184
name: 'Building/fetching previous CI target: equations'
186-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
187-
job "equations"
188-
- if: steps.stepCheck.outputs.status == 'built'
185+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
186+
--argstr job "equations"
187+
- if: steps.stepCheck.outputs.status != 'fetched'
189188
name: 'Building/fetching previous CI target: mathcomp-boot'
190-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
191-
job "mathcomp-boot"
192-
- if: steps.stepCheck.outputs.status == 'built'
189+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
190+
--argstr job "mathcomp-boot"
191+
- if: steps.stepCheck.outputs.status != 'fetched'
193192
name: 'Building/fetching previous CI target: mathcomp-analysis'
194-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
195-
job "mathcomp-analysis"
196-
- if: steps.stepCheck.outputs.status == 'built'
193+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
194+
--argstr job "mathcomp-analysis"
195+
- if: steps.stepCheck.outputs.status != 'fetched'
197196
name: 'Building/fetching previous CI target: mathcomp-experimental-reals'
198-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
199-
job "mathcomp-experimental-reals"
200-
- if: steps.stepCheck.outputs.status == 'built'
197+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
198+
--argstr job "mathcomp-experimental-reals"
199+
- if: steps.stepCheck.outputs.status != 'fetched'
201200
name: 'Building/fetching previous CI target: mathcomp-word'
202-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
203-
job "mathcomp-word"
204-
- if: steps.stepCheck.outputs.status == 'built'
201+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
202+
--argstr job "mathcomp-word"
203+
- if: steps.stepCheck.outputs.status != 'fetched'
205204
name: 'Building/fetching previous CI target: extructures'
206-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
207-
job "extructures"
208-
- if: steps.stepCheck.outputs.status == 'built'
205+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
206+
--argstr job "extructures"
207+
- if: steps.stepCheck.outputs.status != 'fetched'
209208
name: 'Building/fetching previous CI target: deriving'
210-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
211-
job "deriving"
212-
- if: steps.stepCheck.outputs.status == 'built'
209+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
210+
--argstr job "deriving"
211+
- if: steps.stepCheck.outputs.status != 'fetched'
213212
name: Building/fetching current CI target
214-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20" --argstr
215-
job "ssprove"
213+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "8.20"
214+
--argstr job "ssprove"
216215
name: Nix CI for bundle 8.20
217216
on:
218217
pull_request:

0 commit comments

Comments
 (0)