Skip to content

Commit 9e1e1dc

Browse files
garesCohenCyril
gares
and
CohenCyril
committed
Interleaving instance declaration with secion variable postulates
Co-Authored-By: Cyril Cohen <[email protected]>
1 parent 22b5208 commit 9e1e1dc

25 files changed

+989
-973
lines changed

‎.github/workflows/nix-action-coq-8.13.yml‎ renamed to ‎.github/workflows/nix-action-coq-8.15.yml‎

Lines changed: 36 additions & 32 deletions
Original file line numberDiff line numberDiff line change
@@ -28,12 +28,12 @@ jobs:
2828
- id: stepCheck
2929
name: Checking presence of CI target coq
3030
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
31-
\ bundle \"coq-8.13\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
31+
\ bundle \"coq-8.15\" --argstr job \"coq\" \\\n --dry-run 2>&1 > /dev/null)\n\
3232
echo $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run | grep\
3333
\ \"built:\" | sed \"s/.*/built/\")\n"
3434
- if: steps.stepCheck.outputs.status == 'built'
3535
name: Building/fetching current CI target
36-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
36+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
3737
--argstr job "coq"
3838
graph-theory:
3939
needs:
@@ -66,28 +66,32 @@ jobs:
6666
- id: stepCheck
6767
name: Checking presence of CI target graph-theory
6868
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
69-
\ bundle \"coq-8.13\" --argstr job \"graph-theory\" \\\n --dry-run 2>&1\
69+
\ bundle \"coq-8.15\" --argstr job \"graph-theory\" \\\n --dry-run 2>&1\
7070
\ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\
7171
\ | grep \"built:\" | sed \"s/.*/built/\")\n"
7272
- if: steps.stepCheck.outputs.status == 'built'
7373
name: 'Building/fetching previous CI target: coq'
74-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
74+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
7575
--argstr job "coq"
7676
- if: steps.stepCheck.outputs.status == 'built'
7777
name: 'Building/fetching previous CI target: mathcomp-algebra'
78-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
78+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
7979
--argstr job "mathcomp-algebra"
8080
- if: steps.stepCheck.outputs.status == 'built'
8181
name: 'Building/fetching previous CI target: mathcomp-finmap'
82-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
82+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
8383
--argstr job "mathcomp-finmap"
84+
- if: steps.stepCheck.outputs.status == 'built'
85+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
86+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
87+
--argstr job "mathcomp-fingroup"
8488
- if: steps.stepCheck.outputs.status == 'built'
8589
name: 'Building/fetching previous CI target: hierarchy-builder'
86-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
90+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
8791
--argstr job "hierarchy-builder"
8892
- if: steps.stepCheck.outputs.status == 'built'
8993
name: Building/fetching current CI target
90-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
94+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
9195
--argstr job "graph-theory"
9296
hierarchy-builder:
9397
needs:
@@ -119,20 +123,20 @@ jobs:
119123
- id: stepCheck
120124
name: Checking presence of CI target hierarchy-builder
121125
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
122-
\ bundle \"coq-8.13\" --argstr job \"hierarchy-builder\" \\\n --dry-run\
126+
\ bundle \"coq-8.15\" --argstr job \"hierarchy-builder\" \\\n --dry-run\
123127
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
124128
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
125129
- if: steps.stepCheck.outputs.status == 'built'
126130
name: 'Building/fetching previous CI target: coq'
127-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
131+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
128132
--argstr job "coq"
129133
- if: steps.stepCheck.outputs.status == 'built'
130134
name: 'Building/fetching previous CI target: coq-elpi'
131-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
135+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
132136
--argstr job "coq-elpi"
133137
- if: steps.stepCheck.outputs.status == 'built'
134138
name: Building/fetching current CI target
135-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
139+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
136140
--argstr job "hierarchy-builder"
137141
mathcomp-analysis:
138142
needs:
@@ -165,40 +169,40 @@ jobs:
165169
- id: stepCheck
166170
name: Checking presence of CI target mathcomp-analysis
167171
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
168-
\ bundle \"coq-8.13\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\
172+
\ bundle \"coq-8.15\" --argstr job \"mathcomp-analysis\" \\\n --dry-run\
169173
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
170174
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
171175
- if: steps.stepCheck.outputs.status == 'built'
172176
name: 'Building/fetching previous CI target: coq'
173-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
177+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
174178
--argstr job "coq"
175179
- if: steps.stepCheck.outputs.status == 'built'
176180
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
177-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
181+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
178182
--argstr job "mathcomp-ssreflect"
179183
- if: steps.stepCheck.outputs.status == 'built'
180184
name: 'Building/fetching previous CI target: mathcomp-field'
181-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
185+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
182186
--argstr job "mathcomp-field"
183187
- if: steps.stepCheck.outputs.status == 'built'
184188
name: 'Building/fetching previous CI target: mathcomp-finmap'
185-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
189+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
186190
--argstr job "mathcomp-finmap"
187191
- if: steps.stepCheck.outputs.status == 'built'
188192
name: 'Building/fetching previous CI target: mathcomp-bigenough'
189-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
193+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
190194
--argstr job "mathcomp-bigenough"
191195
- if: steps.stepCheck.outputs.status == 'built'
192196
name: 'Building/fetching previous CI target: mathcomp-real-closed'
193-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
197+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
194198
--argstr job "mathcomp-real-closed"
195199
- if: steps.stepCheck.outputs.status == 'built'
196200
name: 'Building/fetching previous CI target: hierarchy-builder'
197-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
201+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
198202
--argstr job "hierarchy-builder"
199203
- if: steps.stepCheck.outputs.status == 'built'
200204
name: Building/fetching current CI target
201-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
205+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
202206
--argstr job "mathcomp-analysis"
203207
mathcomp-single:
204208
needs:
@@ -231,24 +235,24 @@ jobs:
231235
- id: stepCheck
232236
name: Checking presence of CI target mathcomp-single
233237
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
234-
\ bundle \"coq-8.13\" --argstr job \"mathcomp-single\" \\\n --dry-run 2>&1\
238+
\ bundle \"coq-8.15\" --argstr job \"mathcomp-single\" \\\n --dry-run 2>&1\
235239
\ > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo $nb_dry_run\
236240
\ | grep \"built:\" | sed \"s/.*/built/\")\n"
237241
- if: steps.stepCheck.outputs.status == 'built'
238242
name: 'Building/fetching previous CI target: coq'
239-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
243+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
240244
--argstr job "coq"
241245
- if: steps.stepCheck.outputs.status == 'built'
242246
name: 'Building/fetching previous CI target: coq-elpi'
243-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
247+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
244248
--argstr job "coq-elpi"
245249
- if: steps.stepCheck.outputs.status == 'built'
246250
name: 'Building/fetching previous CI target: hierarchy-builder'
247-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
251+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
248252
--argstr job "hierarchy-builder"
249253
- if: steps.stepCheck.outputs.status == 'built'
250254
name: Building/fetching current CI target
251-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
255+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
252256
--argstr job "mathcomp-single"
253257
mathcomp-single-planB-src:
254258
needs:
@@ -281,26 +285,26 @@ jobs:
281285
- id: stepCheck
282286
name: Checking presence of CI target mathcomp-single-planB-src
283287
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
284-
\ bundle \"coq-8.13\" --argstr job \"mathcomp-single-planB-src\" \\\n --dry-run\
288+
\ bundle \"coq-8.15\" --argstr job \"mathcomp-single-planB-src\" \\\n --dry-run\
285289
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho ::set-output name=status::$(echo\
286290
\ $nb_dry_run | grep \"built:\" | sed \"s/.*/built/\")\n"
287291
- if: steps.stepCheck.outputs.status == 'built'
288292
name: 'Building/fetching previous CI target: coq'
289-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
293+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
290294
--argstr job "coq"
291295
- if: steps.stepCheck.outputs.status == 'built'
292296
name: 'Building/fetching previous CI target: coq-elpi'
293-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
297+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
294298
--argstr job "coq-elpi"
295299
- if: steps.stepCheck.outputs.status == 'built'
296300
name: 'Building/fetching previous CI target: hierarchy-builder'
297-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
301+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
298302
--argstr job "hierarchy-builder"
299303
- if: steps.stepCheck.outputs.status == 'built'
300304
name: Building/fetching current CI target
301-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.13"
305+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.15"
302306
--argstr job "mathcomp-single-planB-src"
303-
name: Nix CI for bundle coq-8.13
307+
name: Nix CI for bundle coq-8.15
304308
'on':
305309
pull_request:
306310
paths:

0 commit comments

Comments
 (0)