Skip to content

Commit 577fa14

Browse files
proux01proux01
committed
[CI] Update Nix toolbox
1 parent f141c7e commit 577fa14

File tree

7 files changed

+277
-285
lines changed

7 files changed

+277
-285
lines changed

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

Lines changed: 166 additions & 35 deletions
Original file line numberDiff line numberDiff line change
@@ -74,6 +74,7 @@ jobs:
7474
needs:
7575
- coq
7676
- mathcomp-ssreflect
77+
- stdlib
7778
runs-on: ubuntu-latest
7879
steps:
7980
- name: Determine which commit to initially checkout
@@ -129,6 +130,10 @@ jobs:
129130
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
130131
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
131132
--argstr job "mathcomp-ssreflect"
133+
- if: steps.stepCheck.outputs.status == 'built'
134+
name: 'Building/fetching previous CI target: stdlib'
135+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
136+
--argstr job "stdlib"
132137
- if: steps.stepCheck.outputs.status == 'built'
133138
name: Building/fetching current CI target
134139
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -382,6 +387,7 @@ jobs:
382387
coquelicot:
383388
needs:
384389
- coq
390+
- stdlib
385391
- mathcomp-ssreflect
386392
runs-on: ubuntu-latest
387393
steps:
@@ -434,6 +440,10 @@ jobs:
434440
name: 'Building/fetching previous CI target: coq'
435441
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
436442
--argstr job "coq"
443+
- if: steps.stepCheck.outputs.status == 'built'
444+
name: 'Building/fetching previous CI target: stdlib'
445+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
446+
--argstr job "stdlib"
437447
- if: steps.stepCheck.outputs.status == 'built'
438448
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
439449
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -442,6 +452,77 @@ jobs:
442452
name: Building/fetching current CI target
443453
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
444454
--argstr job "coquelicot"
455+
corn:
456+
needs:
457+
- coq
458+
- coq-elpi
459+
runs-on: ubuntu-latest
460+
steps:
461+
- name: Determine which commit to initially checkout
462+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
463+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
464+
}}\" >> $GITHUB_ENV\nfi\n"
465+
- name: Git checkout
466+
uses: actions/checkout@v4
467+
with:
468+
fetch-depth: 0
469+
ref: ${{ env.target_commit }}
470+
- name: Determine which commit to test
471+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
472+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
473+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
474+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
475+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
476+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
477+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
478+
\ fi\nfi\n"
479+
- name: Git checkout
480+
uses: actions/checkout@v4
481+
with:
482+
fetch-depth: 0
483+
ref: ${{ env.tested_commit }}
484+
- name: Cachix install
485+
uses: cachix/install-nix-action@v30
486+
with:
487+
nix_path: nixpkgs=channel:nixpkgs-unstable
488+
- name: Cachix setup coq-elpi
489+
uses: cachix/cachix-action@v15
490+
with:
491+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
492+
extraPullNames: coq, coq-community, math-comp
493+
name: coq-elpi
494+
- id: stepGetDerivation
495+
name: Getting derivation for current job (corn)
496+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
497+
\"coq-8.20\" --argstr job \"corn\" \\\n --dry-run 2> err > out || (touch
498+
fail; true)\n"
499+
- name: Error reporting
500+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
501+
- name: Failure check
502+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
503+
- id: stepCheck
504+
name: Checking presence of CI target for current job
505+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
506+
- if: steps.stepCheck.outputs.status == 'built'
507+
name: 'Building/fetching previous CI target: coq'
508+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
509+
--argstr job "coq"
510+
- if: steps.stepCheck.outputs.status == 'built'
511+
name: 'Building/fetching previous CI target: bignums'
512+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
513+
--argstr job "bignums"
514+
- if: steps.stepCheck.outputs.status == 'built'
515+
name: 'Building/fetching previous CI target: math-classes'
516+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
517+
--argstr job "math-classes"
518+
- if: steps.stepCheck.outputs.status == 'built'
519+
name: 'Building/fetching previous CI target: coq-elpi'
520+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
521+
--argstr job "coq-elpi"
522+
- if: steps.stepCheck.outputs.status == 'built'
523+
name: Building/fetching current CI target
524+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
525+
--argstr job "corn"
445526
hierarchy-builder:
446527
needs:
447528
- coq
@@ -589,7 +670,6 @@ jobs:
589670
mathcomp:
590671
needs:
591672
- coq
592-
- stdlib
593673
- mathcomp-ssreflect
594674
- mathcomp-fingroup
595675
- mathcomp-algebra
@@ -648,10 +728,6 @@ jobs:
648728
name: 'Building/fetching previous CI target: coq'
649729
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
650730
--argstr job "coq"
651-
- if: steps.stepCheck.outputs.status == 'built'
652-
name: 'Building/fetching previous CI target: stdlib'
653-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
654-
--argstr job "stdlib"
655731
- if: steps.stepCheck.outputs.status == 'built'
656732
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
657733
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -687,7 +763,6 @@ jobs:
687763
mathcomp-algebra:
688764
needs:
689765
- coq
690-
- stdlib
691766
- mathcomp-ssreflect
692767
- mathcomp-fingroup
693768
- hierarchy-builder
@@ -742,10 +817,6 @@ jobs:
742817
name: 'Building/fetching previous CI target: coq'
743818
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
744819
--argstr job "coq"
745-
- if: steps.stepCheck.outputs.status == 'built'
746-
name: 'Building/fetching previous CI target: stdlib'
747-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
748-
--argstr job "stdlib"
749820
- if: steps.stepCheck.outputs.status == 'built'
750821
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
751822
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -845,6 +916,7 @@ jobs:
845916
- coq
846917
- mathcomp-analysis
847918
- mathcomp-reals-stdlib
919+
- stdlib
848920
- hierarchy-builder
849921
runs-on: ubuntu-latest
850922
steps:
@@ -905,6 +977,10 @@ jobs:
905977
name: 'Building/fetching previous CI target: mathcomp-reals-stdlib'
906978
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
907979
--argstr job "mathcomp-reals-stdlib"
980+
- if: steps.stepCheck.outputs.status == 'built'
981+
name: 'Building/fetching previous CI target: stdlib'
982+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
983+
--argstr job "stdlib"
908984
- if: steps.stepCheck.outputs.status == 'built'
909985
name: 'Building/fetching previous CI target: hierarchy-builder'
910986
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -979,7 +1055,6 @@ jobs:
9791055
mathcomp-character:
9801056
needs:
9811057
- coq
982-
- stdlib
9831058
- mathcomp-ssreflect
9841059
- mathcomp-fingroup
9851060
- mathcomp-algebra
@@ -1037,10 +1112,6 @@ jobs:
10371112
name: 'Building/fetching previous CI target: coq'
10381113
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
10391114
--argstr job "coq"
1040-
- if: steps.stepCheck.outputs.status == 'built'
1041-
name: 'Building/fetching previous CI target: stdlib'
1042-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1043-
--argstr job "stdlib"
10441115
- if: steps.stepCheck.outputs.status == 'built'
10451116
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
10461117
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -1218,7 +1289,6 @@ jobs:
12181289
mathcomp-field:
12191290
needs:
12201291
- coq
1221-
- stdlib
12221292
- mathcomp-ssreflect
12231293
- mathcomp-fingroup
12241294
- mathcomp-algebra
@@ -1275,10 +1345,6 @@ jobs:
12751345
name: 'Building/fetching previous CI target: coq'
12761346
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
12771347
--argstr job "coq"
1278-
- if: steps.stepCheck.outputs.status == 'built'
1279-
name: 'Building/fetching previous CI target: stdlib'
1280-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1281-
--argstr job "stdlib"
12821348
- if: steps.stepCheck.outputs.status == 'built'
12831349
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
12841350
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -1306,7 +1372,6 @@ jobs:
13061372
mathcomp-fingroup:
13071373
needs:
13081374
- coq
1309-
- stdlib
13101375
- mathcomp-ssreflect
13111376
- hierarchy-builder
13121377
runs-on: ubuntu-latest
@@ -1360,10 +1425,6 @@ jobs:
13601425
name: 'Building/fetching previous CI target: coq'
13611426
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
13621427
--argstr job "coq"
1363-
- if: steps.stepCheck.outputs.status == 'built'
1364-
name: 'Building/fetching previous CI target: stdlib'
1365-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1366-
--argstr job "stdlib"
13671428
- if: steps.stepCheck.outputs.status == 'built'
13681429
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
13691430
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -1599,6 +1660,7 @@ jobs:
15991660
needs:
16001661
- coq
16011662
- mathcomp-reals
1663+
- stdlib
16021664
- hierarchy-builder
16031665
runs-on: ubuntu-latest
16041666
steps:
@@ -1655,6 +1717,10 @@ jobs:
16551717
name: 'Building/fetching previous CI target: mathcomp-reals'
16561718
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
16571719
--argstr job "mathcomp-reals"
1720+
- if: steps.stepCheck.outputs.status == 'built'
1721+
name: 'Building/fetching previous CI target: stdlib'
1722+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1723+
--argstr job "stdlib"
16581724
- if: steps.stepCheck.outputs.status == 'built'
16591725
name: 'Building/fetching previous CI target: hierarchy-builder'
16601726
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -1666,7 +1732,6 @@ jobs:
16661732
mathcomp-solvable:
16671733
needs:
16681734
- coq
1669-
- stdlib
16701735
- mathcomp-ssreflect
16711736
- mathcomp-fingroup
16721737
- mathcomp-algebra
@@ -1722,10 +1787,6 @@ jobs:
17221787
name: 'Building/fetching previous CI target: coq'
17231788
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
17241789
--argstr job "coq"
1725-
- if: steps.stepCheck.outputs.status == 'built'
1726-
name: 'Building/fetching previous CI target: stdlib'
1727-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1728-
--argstr job "stdlib"
17291790
- if: steps.stepCheck.outputs.status == 'built'
17301791
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
17311792
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -1749,7 +1810,6 @@ jobs:
17491810
mathcomp-ssreflect:
17501811
needs:
17511812
- coq
1752-
- stdlib
17531813
- hierarchy-builder
17541814
runs-on: ubuntu-latest
17551815
steps:
@@ -1802,10 +1862,6 @@ jobs:
18021862
name: 'Building/fetching previous CI target: coq'
18031863
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
18041864
--argstr job "coq"
1805-
- if: steps.stepCheck.outputs.status == 'built'
1806-
name: 'Building/fetching previous CI target: stdlib'
1807-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
1808-
--argstr job "stdlib"
18091865
- if: steps.stepCheck.outputs.status == 'built'
18101866
name: 'Building/fetching previous CI target: hierarchy-builder'
18111867
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
@@ -2115,6 +2171,81 @@ jobs:
21152171
name: Building/fetching current CI target
21162172
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
21172173
--argstr job "stdlib"
2174+
vcfloat:
2175+
needs:
2176+
- coq
2177+
- interval
2178+
runs-on: ubuntu-latest
2179+
steps:
2180+
- name: Determine which commit to initially checkout
2181+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
2182+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
2183+
}}\" >> $GITHUB_ENV\nfi\n"
2184+
- name: Git checkout
2185+
uses: actions/checkout@v4
2186+
with:
2187+
fetch-depth: 0
2188+
ref: ${{ env.target_commit }}
2189+
- name: Determine which commit to test
2190+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
2191+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
2192+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
2193+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
2194+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
2195+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
2196+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
2197+
\ fi\nfi\n"
2198+
- name: Git checkout
2199+
uses: actions/checkout@v4
2200+
with:
2201+
fetch-depth: 0
2202+
ref: ${{ env.tested_commit }}
2203+
- name: Cachix install
2204+
uses: cachix/install-nix-action@v30
2205+
with:
2206+
nix_path: nixpkgs=channel:nixpkgs-unstable
2207+
- name: Cachix setup coq-elpi
2208+
uses: cachix/cachix-action@v15
2209+
with:
2210+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
2211+
extraPullNames: coq, coq-community, math-comp
2212+
name: coq-elpi
2213+
- id: stepGetDerivation
2214+
name: Getting derivation for current job (vcfloat)
2215+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
2216+
\"coq-8.20\" --argstr job \"vcfloat\" \\\n --dry-run 2> err > out || (touch
2217+
fail; true)\n"
2218+
- name: Error reporting
2219+
run: "echo \"out=\"; cat out\necho \"err=\"; cat err\n"
2220+
- name: Failure check
2221+
run: if [ -e fail ]; then exit 1; else exit 0; fi;
2222+
- id: stepCheck
2223+
name: Checking presence of CI target for current job
2224+
run: (echo -n status=; cat out err | grep "built:" | sed "s/.*/built/") >> $GITHUB_OUTPUT
2225+
- if: steps.stepCheck.outputs.status == 'built'
2226+
name: 'Building/fetching previous CI target: coq'
2227+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2228+
--argstr job "coq"
2229+
- if: steps.stepCheck.outputs.status == 'built'
2230+
name: 'Building/fetching previous CI target: interval'
2231+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2232+
--argstr job "interval"
2233+
- if: steps.stepCheck.outputs.status == 'built'
2234+
name: 'Building/fetching previous CI target: compcert'
2235+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2236+
--argstr job "compcert"
2237+
- if: steps.stepCheck.outputs.status == 'built'
2238+
name: 'Building/fetching previous CI target: flocq'
2239+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2240+
--argstr job "flocq"
2241+
- if: steps.stepCheck.outputs.status == 'built'
2242+
name: 'Building/fetching previous CI target: bignums'
2243+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2244+
--argstr job "bignums"
2245+
- if: steps.stepCheck.outputs.status == 'built'
2246+
name: Building/fetching current CI target
2247+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-8.20"
2248+
--argstr job "vcfloat"
21182249
name: Nix CI for bundle coq-8.20
21192250
on:
21202251
pull_request:

0 commit comments

Comments
 (0)