Skip to content

Commit 4a03b4f

Browse files
proux01proux01
committed
WIP
1 parent e8ed4f8 commit 4a03b4f

File tree

1 file changed

+93
-36
lines changed

1 file changed

+93
-36
lines changed

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

+93-36
Original file line numberDiff line numberDiff line change
@@ -1439,10 +1439,11 @@ jobs:
14391439
name: Building/fetching current CI target
14401440
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
14411441
--argstr job "coquelicot"
1442-
coqutil:
1442+
corn:
14431443
needs:
14441444
- coq
1445-
- stdlib
1445+
- bignums
1446+
- math-classes
14461447
runs-on: ubuntu-latest
14471448
steps:
14481449
- name: Determine which commit to initially checkout
@@ -1479,28 +1480,31 @@ jobs:
14791480
extraPullNames: coq, math-comp
14801481
name: coq-community
14811482
- id: stepCheck
1482-
name: Checking presence of CI target coqutil
1483+
name: Checking presence of CI target corn
14831484
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+
\ bundle \"coq-master\" --argstr job \"corn\" \\\n --dry-run 2>&1 > /dev/null)\n\
14851486
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
14861487
s/.*/built/\") >> $GITHUB_OUTPUT\n"
14871488
- if: steps.stepCheck.outputs.status == 'built'
14881489
name: 'Building/fetching previous CI target: coq'
14891490
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
14901491
--argstr job "coq"
14911492
- if: steps.stepCheck.outputs.status == 'built'
1492-
name: 'Building/fetching previous CI target: stdlib'
1493+
name: 'Building/fetching previous CI target: bignums'
14931494
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1494-
--argstr job "stdlib"
1495+
--argstr job "bignums"
1496+
- if: steps.stepCheck.outputs.status == 'built'
1497+
name: 'Building/fetching previous CI target: math-classes'
1498+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1499+
--argstr job "math-classes"
14951500
- if: steps.stepCheck.outputs.status == 'built'
14961501
name: Building/fetching current CI target
14971502
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1498-
--argstr job "coqutil"
1499-
corn:
1503+
--argstr job "corn"
1504+
deriving:
15001505
needs:
15011506
- coq
1502-
- bignums
1503-
- math-classes
1507+
- mathcomp-ssreflect
15041508
runs-on: ubuntu-latest
15051509
steps:
15061510
- name: Determine which commit to initially checkout
@@ -1537,31 +1541,26 @@ jobs:
15371541
extraPullNames: coq, math-comp
15381542
name: coq-community
15391543
- id: stepCheck
1540-
name: Checking presence of CI target corn
1544+
name: Checking presence of CI target deriving
15411545
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1542-
\ bundle \"coq-master\" --argstr job \"corn\" \\\n --dry-run 2>&1 > /dev/null)\n\
1543-
echo $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\" | sed \"\
1544-
s/.*/built/\") >> $GITHUB_OUTPUT\n"
1546+
\ bundle \"coq-master\" --argstr job \"deriving\" \\\n --dry-run 2>&1 >\
1547+
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
1548+
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
15451549
- if: steps.stepCheck.outputs.status == 'built'
15461550
name: 'Building/fetching previous CI target: coq'
15471551
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
15481552
--argstr job "coq"
15491553
- if: steps.stepCheck.outputs.status == 'built'
1550-
name: 'Building/fetching previous CI target: bignums'
1551-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1552-
--argstr job "bignums"
1553-
- if: steps.stepCheck.outputs.status == 'built'
1554-
name: 'Building/fetching previous CI target: math-classes'
1554+
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
15551555
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1556-
--argstr job "math-classes"
1556+
--argstr job "mathcomp-ssreflect"
15571557
- if: steps.stepCheck.outputs.status == 'built'
15581558
name: Building/fetching current CI target
15591559
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1560-
--argstr job "corn"
1561-
deriving:
1560+
--argstr job "deriving"
1561+
dpdgraph:
15621562
needs:
15631563
- coq
1564-
- mathcomp-ssreflect
15651564
runs-on: ubuntu-latest
15661565
steps:
15671566
- name: Determine which commit to initially checkout
@@ -1598,26 +1597,23 @@ jobs:
15981597
extraPullNames: coq, math-comp
15991598
name: coq-community
16001599
- id: stepCheck
1601-
name: Checking presence of CI target deriving
1600+
name: Checking presence of CI target dpdgraph
16021601
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1603-
\ bundle \"coq-master\" --argstr job \"deriving\" \\\n --dry-run 2>&1 >\
1602+
\ bundle \"coq-master\" --argstr job \"dpdgraph\" \\\n --dry-run 2>&1 >\
16041603
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
16051604
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
16061605
- if: steps.stepCheck.outputs.status == 'built'
16071606
name: 'Building/fetching previous CI target: coq'
16081607
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
16091608
--argstr job "coq"
1610-
- if: steps.stepCheck.outputs.status == 'built'
1611-
name: 'Building/fetching previous CI target: mathcomp-ssreflect'
1612-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1613-
--argstr job "mathcomp-ssreflect"
16141609
- if: steps.stepCheck.outputs.status == 'built'
16151610
name: Building/fetching current CI target
16161611
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1617-
--argstr job "deriving"
1618-
dpdgraph:
1612+
--argstr job "dpdgraph"
1613+
engine-bench:
16191614
needs:
16201615
- coq
1616+
- stdlib
16211617
runs-on: ubuntu-latest
16221618
steps:
16231619
- name: Determine which commit to initially checkout
@@ -1654,19 +1650,23 @@ jobs:
16541650
extraPullNames: coq, math-comp
16551651
name: coq-community
16561652
- id: stepCheck
1657-
name: Checking presence of CI target dpdgraph
1653+
name: Checking presence of CI target engine-bench
16581654
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
1659-
\ bundle \"coq-master\" --argstr job \"dpdgraph\" \\\n --dry-run 2>&1 >\
1660-
\ /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"built:\"\
1661-
\ | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
1655+
\ bundle \"coq-master\" --argstr job \"engine-bench\" \\\n --dry-run 2>&1\
1656+
\ > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep \"\
1657+
built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
16621658
- if: steps.stepCheck.outputs.status == 'built'
16631659
name: 'Building/fetching previous CI target: coq'
16641660
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
16651661
--argstr job "coq"
1662+
- if: steps.stepCheck.outputs.status == 'built'
1663+
name: 'Building/fetching previous CI target: stdlib'
1664+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1665+
--argstr job "stdlib"
16661666
- if: steps.stepCheck.outputs.status == 'built'
16671667
name: Building/fetching current CI target
16681668
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
1669-
--argstr job "dpdgraph"
1669+
--argstr job "engine-bench"
16701670
equations:
16711671
needs:
16721672
- coq
@@ -3699,6 +3699,63 @@ jobs:
36993699
name: Building/fetching current CI target
37003700
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
37013701
--argstr job "metacoq-template-coq"
3702+
neural-net-coq-interp:
3703+
needs:
3704+
- coq
3705+
- stdlib
3706+
runs-on: ubuntu-latest
3707+
steps:
3708+
- name: Determine which commit to initially checkout
3709+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{\
3710+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha\
3711+
\ }}\" >> $GITHUB_ENV\nfi\n"
3712+
- name: Git checkout
3713+
uses: actions/checkout@v3
3714+
with:
3715+
fetch-depth: 0
3716+
ref: ${{ env.target_commit }}
3717+
- name: Determine which commit to test
3718+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{\
3719+
\ github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{\
3720+
\ github.event.repository.html_url }} refs/pull/${{ github.event.number }}/merge\
3721+
\ | cut -f1)\n mergeable=$(git merge --no-commit --no-ff ${{ github.event.pull_request.base.sha\
3722+
\ }} > /dev/null 2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n\
3723+
\ if [ -z \"$merge_commit\" -o \"x$mergeable\" != \"x0\" ]; then\n echo\
3724+
\ \"tested_commit=${{ github.event.pull_request.head.sha }}\" >> $GITHUB_ENV\n\
3725+
\ else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n fi\nfi\n"
3726+
- name: Git checkout
3727+
uses: actions/checkout@v3
3728+
with:
3729+
fetch-depth: 0
3730+
ref: ${{ env.tested_commit }}
3731+
- name: Cachix install
3732+
uses: cachix/install-nix-action@v27
3733+
with:
3734+
nix_path: nixpkgs=channel:nixpkgs-unstable
3735+
- name: Cachix setup coq-community
3736+
uses: cachix/cachix-action@v15
3737+
with:
3738+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
3739+
extraPullNames: coq, math-comp
3740+
name: coq-community
3741+
- id: stepCheck
3742+
name: Checking presence of CI target neural-net-coq-interp
3743+
run: "nb_dry_run=$(NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr\
3744+
\ bundle \"coq-master\" --argstr job \"neural-net-coq-interp\" \\\n --dry-run\
3745+
\ 2>&1 > /dev/null)\necho $nb_dry_run\necho status=$(echo $nb_dry_run | grep\
3746+
\ \"built:\" | sed \"s/.*/built/\") >> $GITHUB_OUTPUT\n"
3747+
- if: steps.stepCheck.outputs.status == 'built'
3748+
name: 'Building/fetching previous CI target: coq'
3749+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
3750+
--argstr job "coq"
3751+
- if: steps.stepCheck.outputs.status == 'built'
3752+
name: 'Building/fetching previous CI target: stdlib'
3753+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
3754+
--argstr job "stdlib"
3755+
- if: steps.stepCheck.outputs.status == 'built'
3756+
name: Building/fetching current CI target
3757+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "coq-master"
3758+
--argstr job "neural-net-coq-interp"
37023759
odd-order:
37033760
needs:
37043761
- coq

0 commit comments

Comments
 (0)