Skip to content

Commit e4e487d

Browse files
proux01proux01
authored
Merge pull request #582 from proux01/ci-rocq92
[CI] Add Rocq 9.2
2 parents ccbeb28 + 3e65eca commit e4e487d

5 files changed

Lines changed: 2592 additions & 75 deletions

File tree

‎.github/workflows/nix-action-rocq-9.0.yml‎

Lines changed: 16 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -802,7 +802,6 @@ jobs:
802802
needs:
803803
- coq
804804
- mathcomp-reals
805-
- mathcomp-bigenough
806805
- hierarchy-builder
807806
runs-on: ubuntu-latest
808807
steps:
@@ -860,10 +859,6 @@ jobs:
860859
name: 'Building/fetching previous CI target: mathcomp-reals'
861860
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
862861
"rocq-9.0" --argstr job "mathcomp-reals"
863-
- if: steps.stepCheck.outputs.status != 'fetched'
864-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
865-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
866-
"rocq-9.0" --argstr job "mathcomp-bigenough"
867862
- if: steps.stepCheck.outputs.status != 'fetched'
868863
name: 'Building/fetching previous CI target: hierarchy-builder'
869864
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -952,7 +947,8 @@ jobs:
952947
"rocq-9.0" --argstr job "mathcomp-analysis-stdlib"
953948
mathcomp-bigenough:
954949
needs:
955-
- coq
950+
- rocq-core
951+
- mathcomp-boot
956952
runs-on: ubuntu-latest
957953
steps:
958954
- name: Determine which commit to initially checkout
@@ -1002,9 +998,13 @@ jobs:
1002998
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
1003999
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
10041000
- if: steps.stepCheck.outputs.status != 'fetched'
1005-
name: 'Building/fetching previous CI target: coq'
1001+
name: 'Building/fetching previous CI target: rocq-core'
10061002
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1007-
"rocq-9.0" --argstr job "coq"
1003+
"rocq-9.0" --argstr job "rocq-core"
1004+
- if: steps.stepCheck.outputs.status != 'fetched'
1005+
name: 'Building/fetching previous CI target: mathcomp-boot'
1006+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1007+
"rocq-9.0" --argstr job "mathcomp-boot"
10081008
- if: steps.stepCheck.outputs.status != 'fetched'
10091009
name: Building/fetching current CI target
10101010
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1145,7 +1145,6 @@ jobs:
11451145
mathcomp-classical:
11461146
needs:
11471147
- coq
1148-
- mathcomp-finmap
11491148
- hierarchy-builder
11501149
runs-on: ubuntu-latest
11511150
steps:
@@ -1203,10 +1202,6 @@ jobs:
12031202
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
12041203
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
12051204
"rocq-9.0" --argstr job "mathcomp-ssreflect"
1206-
- if: steps.stepCheck.outputs.status != 'fetched'
1207-
name: 'Building/fetching previous CI target: mathcomp-finmap'
1208-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1209-
"rocq-9.0" --argstr job "mathcomp-finmap"
12101205
- if: steps.stepCheck.outputs.status != 'fetched'
12111206
name: 'Building/fetching previous CI target: hierarchy-builder'
12121207
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1219,7 +1214,6 @@ jobs:
12191214
needs:
12201215
- coq
12211216
- mathcomp-reals
1222-
- mathcomp-bigenough
12231217
- hierarchy-builder
12241218
runs-on: ubuntu-latest
12251219
steps:
@@ -1277,10 +1271,6 @@ jobs:
12771271
name: 'Building/fetching previous CI target: mathcomp-reals'
12781272
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
12791273
"rocq-9.0" --argstr job "mathcomp-reals"
1280-
- if: steps.stepCheck.outputs.status != 'fetched'
1281-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
1282-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1283-
"rocq-9.0" --argstr job "mathcomp-bigenough"
12841274
- if: steps.stepCheck.outputs.status != 'fetched'
12851275
name: 'Building/fetching previous CI target: hierarchy-builder'
12861276
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1429,7 +1419,8 @@ jobs:
14291419
"rocq-9.0" --argstr job "mathcomp-fingroup"
14301420
mathcomp-finmap:
14311421
needs:
1432-
- coq
1422+
- rocq-core
1423+
- mathcomp-boot
14331424
runs-on: ubuntu-latest
14341425
steps:
14351426
- name: Determine which commit to initially checkout
@@ -1479,9 +1470,13 @@ jobs:
14791470
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
14801471
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
14811472
- if: steps.stepCheck.outputs.status != 'fetched'
1482-
name: 'Building/fetching previous CI target: coq'
1473+
name: 'Building/fetching previous CI target: rocq-core'
14831474
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1484-
"rocq-9.0" --argstr job "coq"
1475+
"rocq-9.0" --argstr job "rocq-core"
1476+
- if: steps.stepCheck.outputs.status != 'fetched'
1477+
name: 'Building/fetching previous CI target: mathcomp-boot'
1478+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1479+
"rocq-9.0" --argstr job "mathcomp-boot"
14851480
- if: steps.stepCheck.outputs.status != 'fetched'
14861481
name: Building/fetching current CI target
14871482
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1558,7 +1553,6 @@ jobs:
15581553
mathcomp-real-closed:
15591554
needs:
15601555
- coq
1561-
- mathcomp-bigenough
15621556
runs-on: ubuntu-latest
15631557
steps:
15641558
- name: Determine which commit to initially checkout
@@ -1615,10 +1609,6 @@ jobs:
16151609
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
16161610
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
16171611
"rocq-9.0" --argstr job "mathcomp-ssreflect"
1618-
- if: steps.stepCheck.outputs.status != 'fetched'
1619-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
1620-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1621-
"rocq-9.0" --argstr job "mathcomp-bigenough"
16221612
- if: steps.stepCheck.outputs.status != 'fetched'
16231613
name: Building/fetching current CI target
16241614
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -2031,8 +2021,6 @@ jobs:
20312021
multinomials:
20322022
needs:
20332023
- coq
2034-
- mathcomp-finmap
2035-
- mathcomp-bigenough
20362024
runs-on: ubuntu-latest
20372025
steps:
20382026
- name: Determine which commit to initially checkout
@@ -2085,14 +2073,6 @@ jobs:
20852073
name: 'Building/fetching previous CI target: coq'
20862074
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
20872075
"rocq-9.0" --argstr job "coq"
2088-
- if: steps.stepCheck.outputs.status != 'fetched'
2089-
name: 'Building/fetching previous CI target: mathcomp-finmap'
2090-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2091-
"rocq-9.0" --argstr job "mathcomp-finmap"
2092-
- if: steps.stepCheck.outputs.status != 'fetched'
2093-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
2094-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2095-
"rocq-9.0" --argstr job "mathcomp-bigenough"
20962076
- if: steps.stepCheck.outputs.status != 'fetched'
20972077
name: Building/fetching current CI target
20982078
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

‎.github/workflows/nix-action-rocq-9.1.yml‎

Lines changed: 16 additions & 36 deletions
Original file line numberDiff line numberDiff line change
@@ -802,7 +802,6 @@ jobs:
802802
needs:
803803
- coq
804804
- mathcomp-reals
805-
- mathcomp-bigenough
806805
- hierarchy-builder
807806
runs-on: ubuntu-latest
808807
steps:
@@ -860,10 +859,6 @@ jobs:
860859
name: 'Building/fetching previous CI target: mathcomp-reals'
861860
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
862861
"rocq-9.1" --argstr job "mathcomp-reals"
863-
- if: steps.stepCheck.outputs.status != 'fetched'
864-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
865-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
866-
"rocq-9.1" --argstr job "mathcomp-bigenough"
867862
- if: steps.stepCheck.outputs.status != 'fetched'
868863
name: 'Building/fetching previous CI target: hierarchy-builder'
869864
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -952,7 +947,8 @@ jobs:
952947
"rocq-9.1" --argstr job "mathcomp-analysis-stdlib"
953948
mathcomp-bigenough:
954949
needs:
955-
- coq
950+
- rocq-core
951+
- mathcomp-boot
956952
runs-on: ubuntu-latest
957953
steps:
958954
- name: Determine which commit to initially checkout
@@ -1002,9 +998,13 @@ jobs:
1002998
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
1003999
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
10041000
- if: steps.stepCheck.outputs.status != 'fetched'
1005-
name: 'Building/fetching previous CI target: coq'
1001+
name: 'Building/fetching previous CI target: rocq-core'
10061002
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1007-
"rocq-9.1" --argstr job "coq"
1003+
"rocq-9.1" --argstr job "rocq-core"
1004+
- if: steps.stepCheck.outputs.status != 'fetched'
1005+
name: 'Building/fetching previous CI target: mathcomp-boot'
1006+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1007+
"rocq-9.1" --argstr job "mathcomp-boot"
10081008
- if: steps.stepCheck.outputs.status != 'fetched'
10091009
name: Building/fetching current CI target
10101010
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1145,7 +1145,6 @@ jobs:
11451145
mathcomp-classical:
11461146
needs:
11471147
- coq
1148-
- mathcomp-finmap
11491148
- hierarchy-builder
11501149
runs-on: ubuntu-latest
11511150
steps:
@@ -1203,10 +1202,6 @@ jobs:
12031202
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
12041203
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
12051204
"rocq-9.1" --argstr job "mathcomp-ssreflect"
1206-
- if: steps.stepCheck.outputs.status != 'fetched'
1207-
name: 'Building/fetching previous CI target: mathcomp-finmap'
1208-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1209-
"rocq-9.1" --argstr job "mathcomp-finmap"
12101205
- if: steps.stepCheck.outputs.status != 'fetched'
12111206
name: 'Building/fetching previous CI target: hierarchy-builder'
12121207
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1219,7 +1214,6 @@ jobs:
12191214
needs:
12201215
- coq
12211216
- mathcomp-reals
1222-
- mathcomp-bigenough
12231217
- hierarchy-builder
12241218
runs-on: ubuntu-latest
12251219
steps:
@@ -1277,10 +1271,6 @@ jobs:
12771271
name: 'Building/fetching previous CI target: mathcomp-reals'
12781272
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
12791273
"rocq-9.1" --argstr job "mathcomp-reals"
1280-
- if: steps.stepCheck.outputs.status != 'fetched'
1281-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
1282-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1283-
"rocq-9.1" --argstr job "mathcomp-bigenough"
12841274
- if: steps.stepCheck.outputs.status != 'fetched'
12851275
name: 'Building/fetching previous CI target: hierarchy-builder'
12861276
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1429,7 +1419,8 @@ jobs:
14291419
"rocq-9.1" --argstr job "mathcomp-fingroup"
14301420
mathcomp-finmap:
14311421
needs:
1432-
- coq
1422+
- rocq-core
1423+
- mathcomp-boot
14331424
runs-on: ubuntu-latest
14341425
steps:
14351426
- name: Determine which commit to initially checkout
@@ -1479,9 +1470,13 @@ jobs:
14791470
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
14801471
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
14811472
- if: steps.stepCheck.outputs.status != 'fetched'
1482-
name: 'Building/fetching previous CI target: coq'
1473+
name: 'Building/fetching previous CI target: rocq-core'
14831474
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1484-
"rocq-9.1" --argstr job "coq"
1475+
"rocq-9.1" --argstr job "rocq-core"
1476+
- if: steps.stepCheck.outputs.status != 'fetched'
1477+
name: 'Building/fetching previous CI target: mathcomp-boot'
1478+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1479+
"rocq-9.1" --argstr job "mathcomp-boot"
14851480
- if: steps.stepCheck.outputs.status != 'fetched'
14861481
name: Building/fetching current CI target
14871482
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1558,7 +1553,6 @@ jobs:
15581553
mathcomp-real-closed:
15591554
needs:
15601555
- coq
1561-
- mathcomp-bigenough
15621556
runs-on: ubuntu-latest
15631557
steps:
15641558
- name: Determine which commit to initially checkout
@@ -1615,10 +1609,6 @@ jobs:
16151609
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
16161610
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
16171611
"rocq-9.1" --argstr job "mathcomp-ssreflect"
1618-
- if: steps.stepCheck.outputs.status != 'fetched'
1619-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
1620-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1621-
"rocq-9.1" --argstr job "mathcomp-bigenough"
16221612
- if: steps.stepCheck.outputs.status != 'fetched'
16231613
name: Building/fetching current CI target
16241614
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -2031,8 +2021,6 @@ jobs:
20312021
multinomials:
20322022
needs:
20332023
- coq
2034-
- mathcomp-finmap
2035-
- mathcomp-bigenough
20362024
runs-on: ubuntu-latest
20372025
steps:
20382026
- name: Determine which commit to initially checkout
@@ -2085,14 +2073,6 @@ jobs:
20852073
name: 'Building/fetching previous CI target: coq'
20862074
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
20872075
"rocq-9.1" --argstr job "coq"
2088-
- if: steps.stepCheck.outputs.status != 'fetched'
2089-
name: 'Building/fetching previous CI target: mathcomp-finmap'
2090-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2091-
"rocq-9.1" --argstr job "mathcomp-finmap"
2092-
- if: steps.stepCheck.outputs.status != 'fetched'
2093-
name: 'Building/fetching previous CI target: mathcomp-bigenough'
2094-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2095-
"rocq-9.1" --argstr job "mathcomp-bigenough"
20962076
- if: steps.stepCheck.outputs.status != 'fetched'
20972077
name: Building/fetching current CI target
20982078
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

0 commit comments

Comments
 (0)