Skip to content

Commit 81de981

Browse files
proux01proux01
committed
WIP
1 parent 07a72fa commit 81de981

File tree

1 file changed

+139
-25
lines changed

1 file changed

+139
-25
lines changed

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

+139-25
Original file line numberDiff line numberDiff line change
@@ -1325,10 +1325,10 @@ jobs:
13251325
name: Building/fetching current CI target
13261326
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
13271327
--argstr job "coq-lsp"
1328-
coqprime:
1328+
coq-tools:
13291329
needs:
13301330
- coq
1331-
- bignums
1331+
- stdlib
13321332
runs-on: ubuntu-latest
13331333
steps:
13341334
- name: Determine which commit to initially checkout
@@ -1365,27 +1365,27 @@ jobs:
13651365
extraPullNames: coq, math-comp
13661366
name: coq-community
13671367
- id: stepCheck
1368-
name: Checking presence of CI target coqprime
1368+
name: Checking presence of CI target coq-tools
13691369
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1370-
\ bundle \"coq-master\" --argstr job \"coqprime\" \\\n --dry-run 2>&1 >\
1370+
\ bundle \"coq-master\" --argstr job \"coq-tools\" \\\n --dry-run 2>&1 >\
13711371
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
13721372
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
13731373
- if: steps.stepCheck.outputs.status == 'built'
13741374
name: 'Building/fetching previous CI target: coq'
13751375
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
13761376
--argstr job "coq"
13771377
- if: steps.stepCheck.outputs.status == 'built'
1378-
name: 'Building/fetching previous CI target: bignums'
1378+
name: 'Building/fetching previous CI target: stdlib'
13791379
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1380-
--argstr job "bignums"
1380+
--argstr job "stdlib"
13811381
- if: steps.stepCheck.outputs.status == 'built'
13821382
name: Building/fetching current CI target
13831383
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1384-
--argstr job "coqprime"
1385-
coquelicot:
1384+
--argstr job "coq-tools"
1385+
coqprime:
13861386
needs:
13871387
- coq
1388-
- mathcomp-ssreflect
1388+
- bignums
13891389
runs-on: ubuntu-latest
13901390
steps:
13911391
- name: Determine which commit to initially checkout
@@ -1422,27 +1422,27 @@ jobs:
14221422
extraPullNames: coq, math-comp
14231423
name: coq-community
14241424
- id: stepCheck
1425-
name: Checking presence of CI target coquelicot
1425+
name: Checking presence of CI target coqprime
14261426
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1427-
\ bundle \"coq-master\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1\
1428-
\ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\
1429-
built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
1427+
\ bundle \"coq-master\" --argstr job \"coqprime\" \\\n --dry-run 2>&1 >\
1428+
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
1429+
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
14301430
- if: steps.stepCheck.outputs.status == 'built'
14311431
name: 'Building/fetching previous CI target: coq'
14321432
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
14331433
--argstr job "coq"
14341434
- if: steps.stepCheck.outputs.status == 'built'
1435-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
1435+
name: 'Building/fetching previous CI target: bignums'
14361436
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1437-
--argstr job "mathcomp-ssreflect"
1437+
--argstr job "bignums"
14381438
- if: steps.stepCheck.outputs.status == 'built'
14391439
name: Building/fetching current CI target
14401440
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1441-
--argstr job "coquelicot"
1442-
coqutil:
1441+
--argstr job "coqprime"
1442+
coquelicot:
14431443
needs:
14441444
- coq
1445-
- stdlib
1445+
- mathcomp-ssreflect
14461446
runs-on: ubuntu-latest
14471447
steps:
14481448
- name: Determine which commit to initially checkout
@@ -1479,23 +1479,23 @@ jobs:
14791479
extraPullNames: coq, math-comp
14801480
name: coq-community
14811481
- id: stepCheck
1482-
name: Checking presence of CI target coqutil
1482+
name: Checking presence of CI target coquelicot
14831483
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1484-
\ bundle \"coq-master\" --argstr job \"coqutil\" \\\n --dry-run 2>&1 > /dev/null)\n\
1485-
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
1486-
s/.*/built/\") >> $GITHUB_OUTPUT\n"
1484+
\ bundle \"coq-master\" --argstr job \"coquelicot\" \\\n --dry-run 2>&1\
1485+
\ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\
1486+
built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
14871487
- if: steps.stepCheck.outputs.status == 'built'
14881488
name: 'Building/fetching previous CI target: coq'
14891489
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
14901490
--argstr job "coq"
14911491
- if: steps.stepCheck.outputs.status == 'built'
1492-
name: 'Building/fetching previous CI target: stdlib'
1492+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
14931493
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1494-
--argstr job "stdlib"
1494+
--argstr job "mathcomp-ssreflect"
14951495
- if: steps.stepCheck.outputs.status == 'built'
14961496
name: Building/fetching current CI target
14971497
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1498-
--argstr job "coqutil"
1498+
--argstr job "coquelicot"
14991499
corn:
15001500
needs:
15011501
- coq
@@ -1667,6 +1667,63 @@ jobs:
16671667
name: Building/fetching current CI target
16681668
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
16691669
--argstr job "dpdgraph"
1670+
engine-bench:
1671+
needs:
1672+
- coq
1673+
- stdlib
1674+
runs-on: ubuntu-latest
1675+
steps:
1676+
- name: Determine which commit to initially checkout
1677+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
1678+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
1679+
\ }}\" >> $GITHUB_ENV\nfi\n"
1680+
- name: Git checkout
1681+
uses: actions/checkout@v3
1682+
with:
1683+
fetch-depth: 0
1684+
ref: ${{ env.target_commit }}
1685+
- name: Determine which commit to test
1686+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
1687+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
1688+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
1689+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
1690+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
1691+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
1692+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
1693+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
1694+
- name: Git checkout
1695+
uses: actions/checkout@v3
1696+
with:
1697+
fetch-depth: 0
1698+
ref: ${{ env.tested_commit }}
1699+
- name: Cachix install
1700+
uses: cachix/install-nix-action@v27
1701+
with:
1702+
nix_path: nixpkgs=channel:nixpkgs-unstable
1703+
- name: Cachix setup coq-community
1704+
uses: cachix/cachix-action@v15
1705+
with:
1706+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
1707+
extraPullNames: coq, math-comp
1708+
name: coq-community
1709+
- id: stepCheck
1710+
name: Checking presence of CI target engine-bench
1711+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1712+
\ bundle \"coq-master\" --argstr job \"engine-bench\" \\\n --dry-run 2>&1\
1713+
\ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\
1714+
built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
1715+
- if: steps.stepCheck.outputs.status == 'built'
1716+
name: 'Building/fetching previous CI target: coq'
1717+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1718+
--argstr job "coq"
1719+
- if: steps.stepCheck.outputs.status == 'built'
1720+
name: 'Building/fetching previous CI target: stdlib'
1721+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1722+
--argstr job "stdlib"
1723+
- if: steps.stepCheck.outputs.status == 'built'
1724+
name: Building/fetching current CI target
1725+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1726+
--argstr job "engine-bench"
16701727
equations:
16711728
needs:
16721729
- coq
@@ -3699,6 +3756,63 @@ jobs:
36993756
name: Building/fetching current CI target
37003757
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
37013758
--argstr job "metacoq-template-coq"
3759+
neural-net-coq-interp:
3760+
needs:
3761+
- coq
3762+
- stdlib
3763+
runs-on: ubuntu-latest
3764+
steps:
3765+
- name: Determine which commit to initially checkout
3766+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
3767+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
3768+
\ }}\" >> $GITHUB_ENV\nfi\n"
3769+
- name: Git checkout
3770+
uses: actions/checkout@v3
3771+
with:
3772+
fetch-depth: 0
3773+
ref: ${{ env.target_commit }}
3774+
- name: Determine which commit to test
3775+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
3776+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
3777+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
3778+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
3779+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
3780+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
3781+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
3782+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
3783+
- name: Git checkout
3784+
uses: actions/checkout@v3
3785+
with:
3786+
fetch-depth: 0
3787+
ref: ${{ env.tested_commit }}
3788+
- name: Cachix install
3789+
uses: cachix/install-nix-action@v27
3790+
with:
3791+
nix_path: nixpkgs=channel:nixpkgs-unstable
3792+
- name: Cachix setup coq-community
3793+
uses: cachix/cachix-action@v15
3794+
with:
3795+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
3796+
extraPullNames: coq, math-comp
3797+
name: coq-community
3798+
- id: stepCheck
3799+
name: Checking presence of CI target neural-net-coq-interp
3800+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
3801+
\ bundle \"coq-master\" --argstr job \"neural-net-coq-interp\" \\\n --dry-run\
3802+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
3803+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
3804+
- if: steps.stepCheck.outputs.status == 'built'
3805+
name: 'Building/fetching previous CI target: coq'
3806+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
3807+
--argstr job "coq"
3808+
- if: steps.stepCheck.outputs.status == 'built'
3809+
name: 'Building/fetching previous CI target: stdlib'
3810+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
3811+
--argstr job "stdlib"
3812+
- if: steps.stepCheck.outputs.status == 'built'
3813+
name: Building/fetching current CI target
3814+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
3815+
--argstr job "neural-net-coq-interp"
37023816
odd-order:
37033817
needs:
37043818
- coq

0 commit comments

Comments
 (0)