Skip to content

Commit 72098c0

Browse files
womeierwomeier
authored
test Rocq 9.1 in CI (#17)
1 parent 775932f commit 72098c0

4 files changed

Lines changed: 157 additions & 21 deletions

File tree

‎.github/workflows/nix-action-9.0.yml‎

Lines changed: 20 additions & 20 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,7 @@
11
jobs:
2-
coq:
3-
needs: []
2+
parseque:
3+
needs:
4+
- rocq-core
45
runs-on: ubuntu-latest
56
steps:
67
- name: Determine which commit to initially checkout
@@ -37,10 +38,10 @@ jobs:
3738
extraPullNames: coq
3839
name: coq-community
3940
- id: stepGetDerivation
40-
name: Getting derivation for current job (coq)
41+
name: Getting derivation for current job (parseque)
4142
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
42-
\"9.0\" --argstr job \"coq\" \\\n --dry-run 2> err > out || (touch fail;
43-
true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
43+
\"9.0\" --argstr job \"parseque\" \\\n --dry-run 2> err > out || (touch
44+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
4445
failed\"; exit 1; fi\n"
4546
- id: stepCheck
4647
name: Checking presence of CI target for current job
@@ -49,13 +50,20 @@ jobs:
4950
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
5051
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
5152
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
53+
- if: steps.stepCheck.outputs.status != 'fetched'
54+
name: 'Building/fetching previous CI target: rocq-core'
55+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
56+
job "rocq-core"
57+
- if: steps.stepCheck.outputs.status != 'fetched'
58+
name: 'Building/fetching previous CI target: stdlib'
59+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
60+
job "stdlib"
5261
- if: steps.stepCheck.outputs.status != 'fetched'
5362
name: Building/fetching current CI target
5463
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
55-
job "coq"
56-
parseque:
57-
needs:
58-
- coq
64+
job "parseque"
65+
rocq-core:
66+
needs: []
5967
runs-on: ubuntu-latest
6068
steps:
6169
- name: Determine which commit to initially checkout
@@ -92,9 +100,9 @@ jobs:
92100
extraPullNames: coq
93101
name: coq-community
94102
- id: stepGetDerivation
95-
name: Getting derivation for current job (parseque)
103+
name: Getting derivation for current job (rocq-core)
96104
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
97-
\"9.0\" --argstr job \"parseque\" \\\n --dry-run 2> err > out || (touch
105+
\"9.0\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || (touch
98106
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
99107
failed\"; exit 1; fi\n"
100108
- id: stepCheck
@@ -104,18 +112,10 @@ jobs:
104112
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
105113
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
106114
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
107-
- if: steps.stepCheck.outputs.status != 'fetched'
108-
name: 'Building/fetching previous CI target: coq'
109-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
110-
job "coq"
111-
- if: steps.stepCheck.outputs.status != 'fetched'
112-
name: 'Building/fetching previous CI target: stdlib'
113-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
114-
job "stdlib"
115115
- if: steps.stepCheck.outputs.status != 'fetched'
116116
name: Building/fetching current CI target
117117
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.0" --argstr
118-
job "parseque"
118+
job "rocq-core"
119119
name: Nix CI for bundle 9.0
120120
on:
121121
pull_request:

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

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,133 @@
1+
jobs:
2+
parseque:
3+
needs:
4+
- rocq-core
5+
runs-on: ubuntu-latest
6+
steps:
7+
- name: Determine which commit to initially checkout
8+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
9+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
10+
}}\" >> $GITHUB_ENV\nfi\n"
11+
- name: Git checkout
12+
uses: actions/checkout@v4
13+
with:
14+
fetch-depth: 0
15+
ref: ${{ env.target_commit }}
16+
- name: Determine which commit to test
17+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
18+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
19+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
20+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
21+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
22+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
23+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
24+
\ fi\nfi\n"
25+
- name: Git checkout
26+
uses: actions/checkout@v4
27+
with:
28+
fetch-depth: 0
29+
ref: ${{ env.tested_commit }}
30+
- name: Cachix install
31+
uses: cachix/install-nix-action@v31
32+
with:
33+
nix_path: nixpkgs=channel:nixpkgs-unstable
34+
- name: Cachix setup coq-community
35+
uses: cachix/cachix-action@v16
36+
with:
37+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
38+
extraPullNames: coq
39+
name: coq-community
40+
- id: stepGetDerivation
41+
name: Getting derivation for current job (parseque)
42+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
43+
\"9.1\" --argstr job \"parseque\" \\\n --dry-run 2> err > out || (touch
44+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
45+
failed\"; exit 1; fi\n"
46+
- id: stepCheck
47+
name: Checking presence of CI target for current job
48+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
49+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
50+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
51+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
52+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
53+
- if: steps.stepCheck.outputs.status != 'fetched'
54+
name: 'Building/fetching previous CI target: rocq-core'
55+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" --argstr
56+
job "rocq-core"
57+
- if: steps.stepCheck.outputs.status != 'fetched'
58+
name: 'Building/fetching previous CI target: stdlib'
59+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" --argstr
60+
job "stdlib"
61+
- if: steps.stepCheck.outputs.status != 'fetched'
62+
name: Building/fetching current CI target
63+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" --argstr
64+
job "parseque"
65+
rocq-core:
66+
needs: []
67+
runs-on: ubuntu-latest
68+
steps:
69+
- name: Determine which commit to initially checkout
70+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
71+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
72+
}}\" >> $GITHUB_ENV\nfi\n"
73+
- name: Git checkout
74+
uses: actions/checkout@v4
75+
with:
76+
fetch-depth: 0
77+
ref: ${{ env.target_commit }}
78+
- name: Determine which commit to test
79+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
80+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
81+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
82+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
83+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
84+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
85+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
86+
\ fi\nfi\n"
87+
- name: Git checkout
88+
uses: actions/checkout@v4
89+
with:
90+
fetch-depth: 0
91+
ref: ${{ env.tested_commit }}
92+
- name: Cachix install
93+
uses: cachix/install-nix-action@v31
94+
with:
95+
nix_path: nixpkgs=channel:nixpkgs-unstable
96+
- name: Cachix setup coq-community
97+
uses: cachix/cachix-action@v16
98+
with:
99+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
100+
extraPullNames: coq
101+
name: coq-community
102+
- id: stepGetDerivation
103+
name: Getting derivation for current job (rocq-core)
104+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
105+
\"9.1\" --argstr job \"rocq-core\" \\\n --dry-run 2> err > out || (touch
106+
fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error: getting derivation
107+
failed\"; exit 1; fi\n"
108+
- id: stepCheck
109+
name: Checking presence of CI target for current job
110+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
111+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
112+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
113+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
114+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
115+
- if: steps.stepCheck.outputs.status != 'fetched'
116+
name: Building/fetching current CI target
117+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle "9.1" --argstr
118+
job "rocq-core"
119+
name: Nix CI for bundle 9.1
120+
on:
121+
pull_request:
122+
paths:
123+
- .github/workflows/nix-action-9.1.yml
124+
pull_request_target:
125+
paths-ignore:
126+
- .github/workflows/nix-action-9.1.yml
127+
types:
128+
- opened
129+
- synchronize
130+
- reopened
131+
push:
132+
branches:
133+
- master

‎.nix/config.nix‎

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -10,6 +10,9 @@
1010
bundles."9.0" = {
1111
rocqPackages.rocq-core.override.version = "9.0";
1212
};
13+
bundles."9.1" = {
14+
rocqPackages.rocq-core.override.version = "9.1";
15+
};
1316

1417
## Cachix caches to use in CI
1518
cachix.coq = {};

‎.nix/coq-nix-toolbox.nix‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1 +1 @@
1-
"ca2edb8c74419fdc0a3add0bbd26e4752fe1a457"
1+
"e4f4560d9d6fcc41a5050dfbfca1d46b5f6c0583"

0 commit comments

Comments
 (0)