Skip to content

Commit 3ec3db7

Browse files
proux01proux01
committed
Cleanup after dropping 8.20
1 parent 96db1b4 commit 3ec3db7

File tree

106 files changed

+404
-885
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

106 files changed

+404
-885
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 1 addition & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -20,11 +20,10 @@ jobs:
2020
- 'rocq/rocq-prover:dev'
2121
- 'rocq/rocq-prover:9.1'
2222
- 'rocq/rocq-prover:9.0'
23-
- 'coqorg/coq:8.20'
2423
profile:
2524
- dev
2625
include:
27-
- image: 'coqorg/coq:8.20'
26+
- image: 'rocq/rocq-prover:9.0'
2827
profile: fatalwarnings
2928
fail-fast: false # don't stop jobs if one fails
3029
steps:

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

Lines changed: 64 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -181,60 +181,6 @@ jobs:
181181
name: Building/fetching current CI target
182182
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
183183
"coq-master" --argstr job "coq-elpi"
184-
coq-elpi-tests-stdlib:
185-
needs: []
186-
runs-on: ubuntu-latest
187-
steps:
188-
- name: Determine which commit to initially checkout
189-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
190-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
191-
}}\" >> $GITHUB_ENV\nfi\n"
192-
- name: Git checkout
193-
uses: actions/checkout@v4
194-
with:
195-
fetch-depth: 0
196-
ref: ${{ env.target_commit }}
197-
- name: Determine which commit to test
198-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
199-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
200-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
201-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
202-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
203-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
204-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
205-
\ fi\nfi\n"
206-
- name: Git checkout
207-
uses: actions/checkout@v4
208-
with:
209-
fetch-depth: 0
210-
ref: ${{ env.tested_commit }}
211-
- name: Cachix install
212-
uses: cachix/install-nix-action@v31
213-
with:
214-
nix_path: nixpkgs=channel:nixpkgs-unstable
215-
- name: Cachix setup coq-elpi
216-
uses: cachix/cachix-action@v16
217-
with:
218-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
219-
extraPullNames: coq, coq-community, math-comp
220-
name: coq-elpi
221-
- id: stepGetDerivation
222-
name: Getting derivation for current job (coq-elpi-tests-stdlib)
223-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
224-
\"coq-master\" --argstr job \"coq-elpi-tests-stdlib\" \\\n --dry-run 2>
225-
err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\
226-
Error: getting derivation failed\"; exit 1; fi\n"
227-
- id: stepCheck
228-
name: Checking presence of CI target for current job
229-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
230-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
231-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
232-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
233-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
234-
- if: steps.stepCheck.outputs.status != 'fetched'
235-
name: Building/fetching current CI target
236-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
237-
"coq-master" --argstr job "coq-elpi-tests-stdlib"
238184
coqeal:
239185
needs:
240186
- coq
@@ -2178,6 +2124,70 @@ jobs:
21782124
name: Building/fetching current CI target
21792125
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
21802126
"coq-master" --argstr job "rocq-elpi-tests"
2127+
rocq-elpi-tests-stdlib:
2128+
needs:
2129+
- rocq-core
2130+
- stdlib
2131+
runs-on: ubuntu-latest
2132+
steps:
2133+
- name: Determine which commit to initially checkout
2134+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
2135+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
2136+
}}\" >> $GITHUB_ENV\nfi\n"
2137+
- name: Git checkout
2138+
uses: actions/checkout@v4
2139+
with:
2140+
fetch-depth: 0
2141+
ref: ${{ env.target_commit }}
2142+
- name: Determine which commit to test
2143+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
2144+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
2145+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
2146+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
2147+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
2148+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
2149+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
2150+
\ fi\nfi\n"
2151+
- name: Git checkout
2152+
uses: actions/checkout@v4
2153+
with:
2154+
fetch-depth: 0
2155+
ref: ${{ env.tested_commit }}
2156+
- name: Cachix install
2157+
uses: cachix/install-nix-action@v31
2158+
with:
2159+
nix_path: nixpkgs=channel:nixpkgs-unstable
2160+
- name: Cachix setup coq-elpi
2161+
uses: cachix/cachix-action@v16
2162+
with:
2163+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
2164+
extraPullNames: coq, coq-community, math-comp
2165+
name: coq-elpi
2166+
- id: stepGetDerivation
2167+
name: Getting derivation for current job (rocq-elpi-tests-stdlib)
2168+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
2169+
\"coq-master\" --argstr job \"rocq-elpi-tests-stdlib\" \\\n --dry-run 2>
2170+
err > out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"\
2171+
Error: getting derivation failed\"; exit 1; fi\n"
2172+
- id: stepCheck
2173+
name: Checking presence of CI target for current job
2174+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
2175+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
2176+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
2177+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
2178+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
2179+
- if: steps.stepCheck.outputs.status != 'fetched'
2180+
name: 'Building/fetching previous CI target: rocq-core'
2181+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2182+
"coq-master" --argstr job "rocq-core"
2183+
- if: steps.stepCheck.outputs.status != 'fetched'
2184+
name: 'Building/fetching previous CI target: stdlib'
2185+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2186+
"coq-master" --argstr job "stdlib"
2187+
- if: steps.stepCheck.outputs.status != 'fetched'
2188+
name: Building/fetching current CI target
2189+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2190+
"coq-master" --argstr job "rocq-elpi-tests-stdlib"
21812191
stdlib:
21822192
needs:
21832193
- rocq-core

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

Lines changed: 64 additions & 54 deletions
Original file line numberDiff line numberDiff line change
@@ -250,60 +250,6 @@ jobs:
250250
name: Building/fetching current CI target
251251
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
252252
"rocq-9.0" --argstr job "coq-elpi"
253-
coq-elpi-tests-stdlib:
254-
needs: []
255-
runs-on: ubuntu-latest
256-
steps:
257-
- name: Determine which commit to initially checkout
258-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
259-
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
260-
}}\" >> $GITHUB_ENV\nfi\n"
261-
- name: Git checkout
262-
uses: actions/checkout@v4
263-
with:
264-
fetch-depth: 0
265-
ref: ${{ env.target_commit }}
266-
- name: Determine which commit to test
267-
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
268-
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
269-
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
270-
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
271-
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
272-
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
273-
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
274-
\ fi\nfi\n"
275-
- name: Git checkout
276-
uses: actions/checkout@v4
277-
with:
278-
fetch-depth: 0
279-
ref: ${{ env.tested_commit }}
280-
- name: Cachix install
281-
uses: cachix/install-nix-action@v31
282-
with:
283-
nix_path: nixpkgs=channel:nixpkgs-unstable
284-
- name: Cachix setup coq-elpi
285-
uses: cachix/cachix-action@v16
286-
with:
287-
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
288-
extraPullNames: coq, coq-community, math-comp
289-
name: coq-elpi
290-
- id: stepGetDerivation
291-
name: Getting derivation for current job (coq-elpi-tests-stdlib)
292-
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
293-
\"rocq-9.0\" --argstr job \"coq-elpi-tests-stdlib\" \\\n --dry-run 2> err
294-
> out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error:
295-
getting derivation failed\"; exit 1; fi\n"
296-
- id: stepCheck
297-
name: Checking presence of CI target for current job
298-
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
299-
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
300-
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
301-
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
302-
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
303-
- if: steps.stepCheck.outputs.status != 'fetched'
304-
name: Building/fetching current CI target
305-
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
306-
"rocq-9.0" --argstr job "coq-elpi-tests-stdlib"
307253
coqeal:
308254
needs:
309255
- coq
@@ -2153,6 +2099,70 @@ jobs:
21532099
name: Building/fetching current CI target
21542100
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
21552101
"rocq-9.0" --argstr job "rocq-elpi-tests"
2102+
rocq-elpi-tests-stdlib:
2103+
needs:
2104+
- rocq-core
2105+
- stdlib
2106+
runs-on: ubuntu-latest
2107+
steps:
2108+
- name: Determine which commit to initially checkout
2109+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"target_commit=${{
2110+
github.sha }}\" >> $GITHUB_ENV\nelse\n echo \"target_commit=${{ github.event.pull_request.head.sha
2111+
}}\" >> $GITHUB_ENV\nfi\n"
2112+
- name: Git checkout
2113+
uses: actions/checkout@v4
2114+
with:
2115+
fetch-depth: 0
2116+
ref: ${{ env.target_commit }}
2117+
- name: Determine which commit to test
2118+
run: "if [ ${{ github.event_name }} = \"push\" ]; then\n echo \"tested_commit=${{
2119+
github.sha }}\" >> $GITHUB_ENV\nelse\n merge_commit=$(git ls-remote ${{ github.event.repository.html_url
2120+
}} refs/pull/${{ github.event.number }}/merge | cut -f1)\n mergeable=$(git
2121+
merge --no-commit --no-ff ${{ github.event.pull_request.base.sha }} > /dev/null
2122+
2>&1; echo $?; git merge --abort > /dev/null 2>&1 || true)\n if [ -z \"$merge_commit\"\
2123+
\ -o \"x$mergeable\" != \"x0\" ]; then\n echo \"tested_commit=${{ github.event.pull_request.head.sha
2124+
}}\" >> $GITHUB_ENV\n else\n echo \"tested_commit=$merge_commit\" >> $GITHUB_ENV\n\
2125+
\ fi\nfi\n"
2126+
- name: Git checkout
2127+
uses: actions/checkout@v4
2128+
with:
2129+
fetch-depth: 0
2130+
ref: ${{ env.tested_commit }}
2131+
- name: Cachix install
2132+
uses: cachix/install-nix-action@v31
2133+
with:
2134+
nix_path: nixpkgs=channel:nixpkgs-unstable
2135+
- name: Cachix setup coq-elpi
2136+
uses: cachix/cachix-action@v16
2137+
with:
2138+
authToken: ${{ secrets.CACHIX_AUTH_TOKEN }}
2139+
extraPullNames: coq, coq-community, math-comp
2140+
name: coq-elpi
2141+
- id: stepGetDerivation
2142+
name: Getting derivation for current job (rocq-elpi-tests-stdlib)
2143+
run: "NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link \\\n --argstr bundle
2144+
\"rocq-9.0\" --argstr job \"rocq-elpi-tests-stdlib\" \\\n --dry-run 2> err
2145+
> out || (touch fail; true)\ncat out err\nif [ -e fail ]; then echo \"Error:
2146+
getting derivation failed\"; exit 1; fi\n"
2147+
- id: stepCheck
2148+
name: Checking presence of CI target for current job
2149+
run: "if $(cat out err | grep -q \"built:\") ; then\n echo \"CI target needs
2150+
actual building\"\n if $(cat out err | grep -q \"derivations will be built:\"\
2151+
) ; then\n echo \"waiting a bit for derivations that should be in cache\"\
2152+
\n sleep 30\n fi\nelse\n echo \"CI target already built\"\n echo \"\
2153+
status=fetched\" >> $GITHUB_OUTPUT\nfi\n"
2154+
- if: steps.stepCheck.outputs.status != 'fetched'
2155+
name: 'Building/fetching previous CI target: rocq-core'
2156+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2157+
"rocq-9.0" --argstr job "rocq-core"
2158+
- if: steps.stepCheck.outputs.status != 'fetched'
2159+
name: 'Building/fetching previous CI target: stdlib'
2160+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2161+
"rocq-9.0" --argstr job "stdlib"
2162+
- if: steps.stepCheck.outputs.status != 'fetched'
2163+
name: Building/fetching current CI target
2164+
run: NIXPKGS_ALLOW_UNFREE=1 nix-build --no-out-link --argstr bundle
2165+
"rocq-9.0" --argstr job "rocq-elpi-tests-stdlib"
21562166
stdlib:
21572167
needs:
21582168
- rocq-core

0 commit comments

Comments
 (0)