Skip to content

Commit fb636a8

Browse files
proux01proux01
committed
[CI] Update Nix toolbox
1 parent 20344cf commit fb636a8

File tree

6 files changed

+184
-318
lines changed

6 files changed

+184
-318
lines changed

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

Lines changed: 84 additions & 73 deletions
Original file line numberDiff line numberDiff line change
@@ -327,6 +327,7 @@ jobs:
327327
QuickChick:
328328
needs:
329329
- coq
330+
- mathcomp-boot
330331
- ExtLib
331332
- simple-io
332333
runs-on: ubuntu-latest
@@ -381,6 +382,10 @@ jobs:
381382
name: 'Building/fetching previous CI target: coq'
382383
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
383384
"rocq-9.1" --argstr job "coq"
385+
- if: steps.stepCheck.outputs.status != 'fetched'
386+
name: 'Building/fetching previous CI target: mathcomp-boot'
387+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
388+
"rocq-9.1" --argstr job "mathcomp-boot"
384389
- if: steps.stepCheck.outputs.status != 'fetched'
385390
name: 'Building/fetching previous CI target: ExtLib'
386391
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -462,7 +467,6 @@ jobs:
462467
- coq
463468
- Cheerios
464469
- InfSeqExt
465-
- mathcomp-ssreflect
466470
runs-on: ubuntu-latest
467471
steps:
468472
- name: Determine which commit to initially checkout
@@ -800,6 +804,7 @@ jobs:
800804
autosubst:
801805
needs:
802806
- coq
807+
- mathcomp-boot
803808
- stdlib
804809
runs-on: ubuntu-latest
805810
steps:
@@ -853,6 +858,10 @@ jobs:
853858
name: 'Building/fetching previous CI target: coq'
854859
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
855860
"rocq-9.1" --argstr job "coq"
861+
- if: steps.stepCheck.outputs.status != 'fetched'
862+
name: 'Building/fetching previous CI target: mathcomp-boot'
863+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
864+
"rocq-9.1" --argstr job "mathcomp-boot"
856865
- if: steps.stepCheck.outputs.status != 'fetched'
857866
name: 'Building/fetching previous CI target: stdlib'
858867
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1500,6 +1509,7 @@ jobs:
15001509
needs:
15011510
- coq
15021511
- stdlib
1512+
- mathcomp-boot
15031513
runs-on: ubuntu-latest
15041514
steps:
15051515
- name: Determine which commit to initially checkout
@@ -1556,6 +1566,10 @@ jobs:
15561566
name: 'Building/fetching previous CI target: stdlib'
15571567
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
15581568
"rocq-9.1" --argstr job "stdlib"
1569+
- if: steps.stepCheck.outputs.status != 'fetched'
1570+
name: 'Building/fetching previous CI target: mathcomp-boot'
1571+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1572+
"rocq-9.1" --argstr job "mathcomp-boot"
15591573
- if: steps.stepCheck.outputs.status != 'fetched'
15601574
name: Building/fetching current CI target
15611575
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -1627,7 +1641,6 @@ jobs:
16271641
deriving:
16281642
needs:
16291643
- coq
1630-
- mathcomp-ssreflect
16311644
- stdlib
16321645
runs-on: ubuntu-latest
16331646
steps:
@@ -1824,6 +1837,7 @@ jobs:
18241837
fcsl-pcm:
18251838
needs:
18261839
- coq
1840+
- mathcomp-algebra
18271841
- stdlib
18281842
runs-on: ubuntu-latest
18291843
steps:
@@ -1877,6 +1891,10 @@ jobs:
18771891
name: 'Building/fetching previous CI target: coq'
18781892
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
18791893
"rocq-9.1" --argstr job "coq"
1894+
- if: steps.stepCheck.outputs.status != 'fetched'
1895+
name: 'Building/fetching previous CI target: mathcomp-algebra'
1896+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1897+
"rocq-9.1" --argstr job "mathcomp-algebra"
18801898
- if: steps.stepCheck.outputs.status != 'fetched'
18811899
name: 'Building/fetching previous CI target: stdlib'
18821900
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -2494,7 +2512,7 @@ jobs:
24942512
mathcomp-algebra-tactics:
24952513
needs:
24962514
- coq
2497-
- mathcomp-ssreflect
2515+
- mathcomp-algebra
24982516
- coq-elpi
24992517
- mathcomp-zify
25002518
runs-on: ubuntu-latest
@@ -2553,6 +2571,10 @@ jobs:
25532571
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
25542572
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
25552573
"rocq-9.1" --argstr job "mathcomp-ssreflect"
2574+
- if: steps.stepCheck.outputs.status != 'fetched'
2575+
name: 'Building/fetching previous CI target: mathcomp-algebra'
2576+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2577+
"rocq-9.1" --argstr job "mathcomp-algebra"
25562578
- if: steps.stepCheck.outputs.status != 'fetched'
25572579
name: 'Building/fetching previous CI target: coq-elpi'
25582580
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -2569,6 +2591,7 @@ jobs:
25692591
needs:
25702592
- coq
25712593
- mathcomp-reals
2594+
- mathcomp-field
25722595
- mathcomp-bigenough
25732596
- hierarchy-builder
25742597
runs-on: ubuntu-latest
@@ -2627,6 +2650,10 @@ jobs:
26272650
name: 'Building/fetching previous CI target: mathcomp-reals'
26282651
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
26292652
"rocq-9.1" --argstr job "mathcomp-reals"
2653+
- if: steps.stepCheck.outputs.status != 'fetched'
2654+
name: 'Building/fetching previous CI target: mathcomp-field'
2655+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2656+
"rocq-9.1" --argstr job "mathcomp-field"
26302657
- if: steps.stepCheck.outputs.status != 'fetched'
26312658
name: 'Building/fetching previous CI target: mathcomp-bigenough'
26322659
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -2720,7 +2747,8 @@ jobs:
27202747
"rocq-9.1" --argstr job "mathcomp-analysis-stdlib"
27212748
mathcomp-bigenough:
27222749
needs:
2723-
- coq
2750+
- rocq-core
2751+
- mathcomp-boot
27242752
runs-on: ubuntu-latest
27252753
steps:
27262754
- name: Determine which commit to initially checkout
@@ -2770,9 +2798,13 @@ jobs:
27702798
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
27712799
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
27722800
- if: steps.stepCheck.outputs.status != 'fetched'
2773-
name: 'Building/fetching previous CI target: coq'
2801+
name: 'Building/fetching previous CI target: rocq-core'
27742802
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2775-
"rocq-9.1" --argstr job "coq"
2803+
"rocq-9.1" --argstr job "rocq-core"
2804+
- if: steps.stepCheck.outputs.status != 'fetched'
2805+
name: 'Building/fetching previous CI target: mathcomp-boot'
2806+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2807+
"rocq-9.1" --argstr job "mathcomp-boot"
27762808
- if: steps.stepCheck.outputs.status != 'fetched'
27772809
name: Building/fetching current CI target
27782810
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -2913,7 +2945,7 @@ jobs:
29132945
mathcomp-classical:
29142946
needs:
29152947
- coq
2916-
- mathcomp-ssreflect
2948+
- mathcomp-algebra
29172949
- mathcomp-finmap
29182950
- hierarchy-builder
29192951
runs-on: ubuntu-latest
@@ -2972,6 +3004,10 @@ jobs:
29723004
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
29733005
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
29743006
"rocq-9.1" --argstr job "mathcomp-ssreflect"
3007+
- if: steps.stepCheck.outputs.status != 'fetched'
3008+
name: 'Building/fetching previous CI target: mathcomp-algebra'
3009+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3010+
"rocq-9.1" --argstr job "mathcomp-algebra"
29753011
- if: steps.stepCheck.outputs.status != 'fetched'
29763012
name: 'Building/fetching previous CI target: mathcomp-finmap'
29773013
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -3124,7 +3160,8 @@ jobs:
31243160
"rocq-9.1" --argstr job "mathcomp-fingroup"
31253161
mathcomp-finmap:
31263162
needs:
3127-
- coq
3163+
- rocq-core
3164+
- mathcomp-boot
31283165
runs-on: ubuntu-latest
31293166
steps:
31303167
- name: Determine which commit to initially checkout
@@ -3174,9 +3211,13 @@ jobs:
31743211
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
31753212
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
31763213
- if: steps.stepCheck.outputs.status != 'fetched'
3177-
name: 'Building/fetching previous CI target: coq'
3214+
name: 'Building/fetching previous CI target: rocq-core'
31783215
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3179-
"rocq-9.1" --argstr job "coq"
3216+
"rocq-9.1" --argstr job "rocq-core"
3217+
- if: steps.stepCheck.outputs.status != 'fetched'
3218+
name: 'Building/fetching previous CI target: mathcomp-boot'
3219+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3220+
"rocq-9.1" --argstr job "mathcomp-boot"
31803221
- if: steps.stepCheck.outputs.status != 'fetched'
31813222
name: Building/fetching current CI target
31823223
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -3462,69 +3503,11 @@ jobs:
34623503
name: Building/fetching current CI target
34633504
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
34643505
"rocq-9.1" --argstr job "mathcomp-solvable"
3465-
mathcomp-ssreflect:
3466-
needs:
3467-
- coq
3468-
runs-on: ubuntu-latest
3469-
steps:
3470-
- name: Determine which commit to initially checkout
3471-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
3472-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
3473-
}}\" >> $GITHUB_ENV\nfi\n"
3474-
- name: Git checkout
3475-
uses: actions/checkout@v6
3476-
with:
3477-
fetch-depth: 0
3478-
ref: ${{ env.target_commit }}
3479-
- name: Determine which commit to test
3480-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
3481-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
3482-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
3483-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
3484-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
3485-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
3486-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
3487-
\ fi\nfi\n"
3488-
- name: Git checkout
3489-
uses: actions/checkout@v6
3490-
with:
3491-
fetch-depth: 0
3492-
ref: ${{ env.tested_commit }}
3493-
- name: Cachix install
3494-
uses: cachix/install-nix-action@v31
3495-
with:
3496-
nix_path: nixpkgs=channel:nixpkgs-unstable
3497-
- name: Cachix setup coq
3498-
uses: cachix/cachix-action@v16
3499-
with:
3500-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
3501-
extraPullNames: coq-community, math-comp
3502-
name: coq
3503-
- id: stepGetDerivation
3504-
name: Getting derivation for current job (mathcomp-ssreflect)
3505-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
3506-
\"rocq-9.1\" --argstr job \"mathcomp-ssreflect\" \\\n --dry-run 2> err >
3507-
out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error:
3508-
getting derivation failed\"; exit 1; fi\n"
3509-
- id: stepCheck
3510-
name: Checking presence of CI target for current job
3511-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
3512-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
3513-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
3514-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
3515-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
3516-
- if: steps.stepCheck.outputs.status != 'fetched'
3517-
name: 'Building/fetching previous CI target: coq'
3518-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3519-
"rocq-9.1" --argstr job "coq"
3520-
- if: steps.stepCheck.outputs.status != 'fetched'
3521-
name: Building/fetching current CI target
3522-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3523-
"rocq-9.1" --argstr job "mathcomp-ssreflect"
35243506
mathcomp-word:
35253507
needs:
35263508
- coq
3527-
- mathcomp-ssreflect
3509+
- mathcomp-algebra
3510+
- mathcomp-fingroup
35283511
- stdlib
35293512
runs-on: ubuntu-latest
35303513
steps:
@@ -3578,10 +3561,18 @@ jobs:
35783561
name: 'Building/fetching previous CI target: coq'
35793562
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
35803563
"rocq-9.1" --argstr job "coq"
3564+
- if: steps.stepCheck.outputs.status != 'fetched'
3565+
name: 'Building/fetching previous CI target: mathcomp-algebra'
3566+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3567+
"rocq-9.1" --argstr job "mathcomp-algebra"
35813568
- if: steps.stepCheck.outputs.status != 'fetched'
35823569
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
35833570
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
35843571
"rocq-9.1" --argstr job "mathcomp-ssreflect"
3572+
- if: steps.stepCheck.outputs.status != 'fetched'
3573+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
3574+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3575+
"rocq-9.1" --argstr job "mathcomp-fingroup"
35853576
- if: steps.stepCheck.outputs.status != 'fetched'
35863577
name: 'Building/fetching previous CI target: stdlib'
35873578
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -3593,6 +3584,9 @@ jobs:
35933584
mathcomp-zify:
35943585
needs:
35953586
- coq
3587+
- mathcomp-boot
3588+
- mathcomp-algebra
3589+
- mathcomp-fingroup
35963590
- stdlib
35973591
runs-on: ubuntu-latest
35983592
steps:
@@ -3646,6 +3640,18 @@ jobs:
36463640
name: 'Building/fetching previous CI target: coq'
36473641
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
36483642
"rocq-9.1" --argstr job "coq"
3643+
- if: steps.stepCheck.outputs.status != 'fetched'
3644+
name: 'Building/fetching previous CI target: mathcomp-boot'
3645+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3646+
"rocq-9.1" --argstr job "mathcomp-boot"
3647+
- if: steps.stepCheck.outputs.status != 'fetched'
3648+
name: 'Building/fetching previous CI target: mathcomp-algebra'
3649+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3650+
"rocq-9.1" --argstr job "mathcomp-algebra"
3651+
- if: steps.stepCheck.outputs.status != 'fetched'
3652+
name: 'Building/fetching previous CI target: mathcomp-fingroup'
3653+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3654+
"rocq-9.1" --argstr job "mathcomp-fingroup"
36493655
- if: steps.stepCheck.outputs.status != 'fetched'
36503656
name: 'Building/fetching previous CI target: stdlib'
36513657
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -4323,6 +4329,7 @@ jobs:
43234329
needs:
43244330
- coq
43254331
- aac-tactics
4332+
- mathcomp-boot
43264333
runs-on: ubuntu-latest
43274334
steps:
43284335
- name: Determine which commit to initially checkout
@@ -4379,6 +4386,10 @@ jobs:
43794386
name: 'Building/fetching previous CI target: aac-tactics'
43804387
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
43814388
"rocq-9.1" --argstr job "aac-tactics"
4389+
- if: steps.stepCheck.outputs.status != 'fetched'
4390+
name: 'Building/fetching previous CI target: mathcomp-boot'
4391+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4392+
"rocq-9.1" --argstr job "mathcomp-boot"
43824393
- if: steps.stepCheck.outputs.status != 'fetched'
43834394
name: Building/fetching current CI target
43844395
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -5010,7 +5021,7 @@ jobs:
50105021
"rocq-9.1" --argstr job "stdlib-refman-html"
50115022
stdpp:
50125023
needs:
5013-
- coq
5024+
- rocq-core
50145025
- stdlib
50155026
runs-on: ubuntu-latest
50165027
steps:
@@ -5061,9 +5072,9 @@ jobs:
50615072
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
50625073
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
50635074
- if: steps.stepCheck.outputs.status != 'fetched'
5064-
name: 'Building/fetching previous CI target: coq'
5075+
name: 'Building/fetching previous CI target: rocq-core'
50655076
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
5066-
"rocq-9.1" --argstr job "coq"
5077+
"rocq-9.1" --argstr job "rocq-core"
50675078
- if: steps.stepCheck.outputs.status != 'fetched'
50685079
name: 'Building/fetching previous CI target: stdlib'
50695080
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle

0 commit comments

Comments
 (0)