@@ -1249,70 +1249,6 @@ jobs:
12491249 name : Building/fetching current CI target
12501250 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
12511251 " rocq-9.1" --argstr job "coq"
1252- coq-elpi :
1253- needs :
1254- - coq
1255- - rocq-elpi
1256- runs-on : ubuntu-latest
1257- steps :
1258- - name : Determine which commit to initially checkout
1259- run : " if [ ${{ github.event_name }} = \" push\" ]; then\n echo \" target_commit=${{
1260- github.sha }}\" >> $GITHUB_ENV\n else\n echo \" target_commit=${{ github.event.pull_request.head.sha
1261- }}\" >> $GITHUB_ENV\n fi\n "
1262- - name : Git checkout
1263- uses : actions/checkout@v6
1264- with :
1265- fetch-depth : 0
1266- ref : ${{ env.target_commit }}
1267- - name : Determine which commit to test
1268- run : " if [ ${{ github.event_name }} = \" push\" ]; then\n echo \" tested_commit=${{
1269- github.sha }}\" >> $GITHUB_ENV\n else\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
1270- }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
1271- merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
1272- 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \" $merge_commit\" \
1273- \ -o \" x$mergeable\" != \" x0\" ]; then\n echo \" tested_commit=${{ github.event.pull_request.head.sha
1274- }}\" >> $GITHUB_ENV\n else\n echo \" tested_commit=$merge_commit\" >> $GITHUB_ENV\n \
1275- \ fi\n fi\n "
1276- - name : Git checkout
1277- uses : actions/checkout@v6
1278- with :
1279- fetch-depth : 0
1280- ref : ${{ env.tested_commit }}
1281- - name : Cachix install
1282- uses : cachix/install-nix-action@v31
1283- with :
1284- nix_path : nixpkgs=channel:nixpkgs-unstable
1285- - name : Cachix setup coq
1286- uses : cachix/cachix-action@v16
1287- with :
1288- authToken : ${{ secrets.CACHIX_AUTH_TOKEN }}
1289- extraPullNames : coq-community, math-comp
1290- name : coq
1291- - id : stepGetDerivation
1292- name : Getting derivation for current job (coq-elpi)
1293- run : " NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
1294- \" rocq-9.1\" --argstr job \" coq-elpi\" \\\n --dry-run 2> err > out || (touch
1295- fail; true)\n cat out err\n if [ -e fail ]; then echo \" Error: getting derivation
1296- failed\" ; exit 1; fi\n "
1297- - id : stepCheck
1298- name : Checking presence of CI target for current job
1299- run : " if $(cat out err | grep -q \" built:\" ) ; then\n echo \" CI target needs
1300- actual building\"\n if $(cat out err | grep -q \" derivations will be built:\" \
1301- ) ; then\n echo \" waiting a bit for derivations that should be in cache\" \
1302- \n sleep 30\n fi\n else\n echo \" CI target already built\"\n echo \" \
1303- status=fetched\" >> $GITHUB_OUTPUT\n fi\n "
1304- - if : steps.stepCheck.outputs.status != 'fetched'
1305- name : ' Building/fetching previous CI target: coq'
1306- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1307- " rocq-9.1" --argstr job "coq"
1308- - if : steps.stepCheck.outputs.status != 'fetched'
1309- name : ' Building/fetching previous CI target: rocq-elpi'
1310- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1311- " rocq-9.1" --argstr job "rocq-elpi"
1312- - if : steps.stepCheck.outputs.status != 'fetched'
1313- name : Building/fetching current CI target
1314- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
1315- " rocq-9.1" --argstr job "coq-elpi"
13161252 coq-hammer :
13171253 needs :
13181254 - coq
@@ -1970,7 +1906,6 @@ jobs:
19701906 hierarchy-builder :
19711907 needs :
19721908 - rocq-core
1973- - rocq-elpi
19741909 runs-on : ubuntu-latest
19751910 steps :
19761911 - name : Determine which commit to initially checkout
@@ -2513,7 +2448,6 @@ jobs:
25132448 needs :
25142449 - coq
25152450 - mathcomp-algebra
2516- - coq-elpi
25172451 - mathcomp-zify
25182452 runs-on : ubuntu-latest
25192453 steps :
@@ -2575,10 +2509,6 @@ jobs:
25752509 name : ' Building/fetching previous CI target: mathcomp-algebra'
25762510 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
25772511 " rocq-9.1" --argstr job "mathcomp-algebra"
2578- - if : steps.stepCheck.outputs.status != 'fetched'
2579- name : ' Building/fetching previous CI target: coq-elpi'
2580- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2581- " rocq-9.1" --argstr job "coq-elpi"
25822512 - if : steps.stepCheck.outputs.status != 'fetched'
25832513 name : ' Building/fetching previous CI target: mathcomp-zify'
25842514 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -3664,6 +3594,8 @@ jobs:
36643594 needs :
36653595 - coq
36663596 - equations
3597+ - ExtLib
3598+ - stdlib
36673599 - metarocq-utils
36683600 runs-on : ubuntu-latest
36693601 steps :
@@ -3721,6 +3653,14 @@ jobs:
37213653 name : ' Building/fetching previous CI target: equations'
37223654 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
37233655 " rocq-9.1" --argstr job "equations"
3656+ - if : steps.stepCheck.outputs.status != 'fetched'
3657+ name : ' Building/fetching previous CI target: ExtLib'
3658+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3659+ " rocq-9.1" --argstr job "ExtLib"
3660+ - if : steps.stepCheck.outputs.status != 'fetched'
3661+ name : ' Building/fetching previous CI target: stdlib'
3662+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3663+ " rocq-9.1" --argstr job "stdlib"
37243664 - if : steps.stepCheck.outputs.status != 'fetched'
37253665 name : ' Building/fetching previous CI target: metarocq-utils'
37263666 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -3733,6 +3673,8 @@ jobs:
37333673 needs :
37343674 - coq
37353675 - equations
3676+ - ExtLib
3677+ - stdlib
37363678 - metarocq-common
37373679 runs-on : ubuntu-latest
37383680 steps :
@@ -3790,6 +3732,14 @@ jobs:
37903732 name : ' Building/fetching previous CI target: equations'
37913733 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
37923734 " rocq-9.1" --argstr job "equations"
3735+ - if : steps.stepCheck.outputs.status != 'fetched'
3736+ name : ' Building/fetching previous CI target: ExtLib'
3737+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3738+ " rocq-9.1" --argstr job "ExtLib"
3739+ - if : steps.stepCheck.outputs.status != 'fetched'
3740+ name : ' Building/fetching previous CI target: stdlib'
3741+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3742+ " rocq-9.1" --argstr job "stdlib"
37933743 - if : steps.stepCheck.outputs.status != 'fetched'
37943744 name : ' Building/fetching previous CI target: metarocq-common'
37953745 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -3802,6 +3752,8 @@ jobs:
38023752 needs :
38033753 - coq
38043754 - equations
3755+ - ExtLib
3756+ - stdlib
38053757 - metarocq-template-rocq
38063758 runs-on : ubuntu-latest
38073759 steps :
@@ -3859,6 +3811,14 @@ jobs:
38593811 name : ' Building/fetching previous CI target: equations'
38603812 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
38613813 " rocq-9.1" --argstr job "equations"
3814+ - if : steps.stepCheck.outputs.status != 'fetched'
3815+ name : ' Building/fetching previous CI target: ExtLib'
3816+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3817+ " rocq-9.1" --argstr job "ExtLib"
3818+ - if : steps.stepCheck.outputs.status != 'fetched'
3819+ name : ' Building/fetching previous CI target: stdlib'
3820+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3821+ " rocq-9.1" --argstr job "stdlib"
38623822 - if : steps.stepCheck.outputs.status != 'fetched'
38633823 name : ' Building/fetching previous CI target: metarocq-template-rocq'
38643824 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -3871,6 +3831,8 @@ jobs:
38713831 needs :
38723832 - coq
38733833 - equations
3834+ - ExtLib
3835+ - stdlib
38743836 runs-on : ubuntu-latest
38753837 steps :
38763838 - name : Determine which commit to initially checkout
@@ -3927,6 +3889,14 @@ jobs:
39273889 name : ' Building/fetching previous CI target: equations'
39283890 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
39293891 " rocq-9.1" --argstr job "equations"
3892+ - if : steps.stepCheck.outputs.status != 'fetched'
3893+ name : ' Building/fetching previous CI target: ExtLib'
3894+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3895+ " rocq-9.1" --argstr job "ExtLib"
3896+ - if : steps.stepCheck.outputs.status != 'fetched'
3897+ name : ' Building/fetching previous CI target: stdlib'
3898+ run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
3899+ " rocq-9.1" --argstr job "stdlib"
39303900 - if : steps.stepCheck.outputs.status != 'fetched'
39313901 name : Building/fetching current CI target
39323902 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
@@ -4448,70 +4418,9 @@ jobs:
44484418 name : Building/fetching current CI target
44494419 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
44504420 " rocq-9.1" --argstr job "rocq-core"
4451- rocq-elpi :
4452- needs :
4453- - rocq-core
4454- runs-on : ubuntu-latest
4455- steps :
4456- - name : Determine which commit to initially checkout
4457- run : " if [ ${{ github.event_name }} = \" push\" ]; then\n echo \" target_commit=${{
4458- github.sha }}\" >> $GITHUB_ENV\n else\n echo \" target_commit=${{ github.event.pull_request.head.sha
4459- }}\" >> $GITHUB_ENV\n fi\n "
4460- - name : Git checkout
4461- uses : actions/checkout@v6
4462- with :
4463- fetch-depth : 0
4464- ref : ${{ env.target_commit }}
4465- - name : Determine which commit to test
4466- run : " if [ ${{ github.event_name }} = \" push\" ]; then\n echo \" tested_commit=${{
4467- github.sha }}\" >> $GITHUB_ENV\n else\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
4468- }} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
4469- merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
4470- 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \" $merge_commit\" \
4471- \ -o \" x$mergeable\" != \" x0\" ]; then\n echo \" tested_commit=${{ github.event.pull_request.head.sha
4472- }}\" >> $GITHUB_ENV\n else\n echo \" tested_commit=$merge_commit\" >> $GITHUB_ENV\n \
4473- \ fi\n fi\n "
4474- - name : Git checkout
4475- uses : actions/checkout@v6
4476- with :
4477- fetch-depth : 0
4478- ref : ${{ env.tested_commit }}
4479- - name : Cachix install
4480- uses : cachix/install-nix-action@v31
4481- with :
4482- nix_path : nixpkgs=channel:nixpkgs-unstable
4483- - name : Cachix setup coq
4484- uses : cachix/cachix-action@v16
4485- with :
4486- authToken : ${{ secrets.CACHIX_AUTH_TOKEN }}
4487- extraPullNames : coq-community, math-comp
4488- name : coq
4489- - id : stepGetDerivation
4490- name : Getting derivation for current job (rocq-elpi)
4491- run : " NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
4492- \" rocq-9.1\" --argstr job \" rocq-elpi\" \\\n --dry-run 2> err > out || (touch
4493- fail; true)\n cat out err\n if [ -e fail ]; then echo \" Error: getting derivation
4494- failed\" ; exit 1; fi\n "
4495- - id : stepCheck
4496- name : Checking presence of CI target for current job
4497- run : " if $(cat out err | grep -q \" built:\" ) ; then\n echo \" CI target needs
4498- actual building\"\n if $(cat out err | grep -q \" derivations will be built:\" \
4499- ) ; then\n echo \" waiting a bit for derivations that should be in cache\" \
4500- \n sleep 30\n fi\n else\n echo \" CI target already built\"\n echo \" \
4501- status=fetched\" >> $GITHUB_OUTPUT\n fi\n "
4502- - if : steps.stepCheck.outputs.status != 'fetched'
4503- name : ' Building/fetching previous CI target: rocq-core'
4504- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4505- " rocq-9.1" --argstr job "rocq-core"
4506- - if : steps.stepCheck.outputs.status != 'fetched'
4507- name : Building/fetching current CI target
4508- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4509- " rocq-9.1" --argstr job "rocq-elpi"
45104421 rocq-elpi-test :
45114422 needs :
4512- - rocq-core
4513- - rocq-elpi
4514- - stdlib
4423+ - coq
45154424 runs-on : ubuntu-latest
45164425 steps :
45174426 - name : Determine which commit to initially checkout
@@ -4561,17 +4470,9 @@ jobs:
45614470 \n sleep 30\n fi\n else\n echo \" CI target already built\"\n echo \" \
45624471 status=fetched\" >> $GITHUB_OUTPUT\n fi\n "
45634472 - if : steps.stepCheck.outputs.status != 'fetched'
4564- name : ' Building/fetching previous CI target: rocq-core'
4565- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4566- " rocq-9.1" --argstr job "rocq-core"
4567- - if : steps.stepCheck.outputs.status != 'fetched'
4568- name : ' Building/fetching previous CI target: rocq-elpi'
4569- run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4570- " rocq-9.1" --argstr job "rocq-elpi"
4571- - if : steps.stepCheck.outputs.status != 'fetched'
4572- name : ' Building/fetching previous CI target: stdlib'
4473+ name : ' Building/fetching previous CI target: coq'
45734474 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
4574- " rocq-9.1" --argstr job "stdlib "
4475+ " rocq-9.1" --argstr job "coq "
45754476 - if : steps.stepCheck.outputs.status != 'fetched'
45764477 name : Building/fetching current CI target
45774478 run : NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
0 commit comments