Skip to content

Commit 51ccaaf

Browse files
AlizterAlizter
authored
Merge pull request #2338 from Alizter/push-pzvttwlunlxm
ci: bump minimal rocq version and improve ci
2 parents 1e59841 + b160044 commit 51ccaaf

File tree

3 files changed

+43
-73
lines changed

3 files changed

+43
-73
lines changed

‎.github/workflows/ci.yml‎

Lines changed: 40 additions & 70 deletions
Original file line numberDiff line numberDiff line change
@@ -6,9 +6,12 @@ concurrency:
66
group: "${{ github.workflow }} @ ${{ github.event.pull_request.head.label || github.head_ref || github.ref }}"
77
cancel-in-progress: true
88

9-
# We set the supported coq-version from here. In order to use this environment variable correctly, look at how they are used in the following jobs.
9+
# Coq version configuration
10+
# - coq-version-supported: The main supported version used for documentation
11+
# - Other versions are tested but docs are only built with supported version
1012
env:
11-
coq-version-supported: '8.19'
13+
coq-version-supported: '9.0'
14+
coq-version-9-1: '9.1'
1215
ocaml-version: '4.14-flambda'
1316
deployment-branch: 'gh-pages'
1417

@@ -34,28 +37,21 @@ jobs:
3437
strategy:
3538
fail-fast: false
3639
matrix:
37-
coq-version-dummy:
38-
- 'supported'
39-
- 'latest'
40-
- 'dev'
40+
coq-version:
41+
- '9.0'
42+
- '9.1'
43+
- 'dev'
4144
os:
4245
- ubuntu-latest
43-
env:
44-
coq-version: ${{ matrix.coq-version-dummy }}
4546
runs-on: ${{ matrix.os }}
4647
steps:
47-
# Github actions doesn't let us set workflow level environment variables inside the strategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment variable env.coq-version, which uses the globally set coq-version-supported when running the 'supported' case.
48-
- name: Set supported coq-version
49-
if: matrix.coq-version-dummy == 'supported'
50-
run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
51-
5248
- name: Checkout repo
5349
uses: actions/checkout@v4
5450
- name: Build HoTT
5551
uses: coq-community/[email protected]
5652
with:
5753
opam_file: 'coq-hott.opam'
58-
coq_version: ${{ env.coq-version }}
54+
coq_version: ${{ matrix.coq-version }}
5955
ocaml_version: ${{ env.ocaml-version }}
6056
export: 'OPAMWITHTEST'
6157
env:
@@ -66,26 +62,20 @@ jobs:
6662
strategy:
6763
fail-fast: false
6864
matrix:
69-
coq-version-dummy:
70-
- 'supported'
71-
- 'latest'
72-
- 'dev'
65+
coq-version:
66+
- '9.0'
67+
- '9.1'
68+
- 'dev'
7369
os:
74-
- ubuntu-latest
75-
env:
76-
coq-version: ${{ matrix.coq-version-dummy }}
70+
- ubuntu-latest
7771
runs-on: ${{ matrix.os }}
7872
steps:
79-
# Github actions doesn't let us set workflow level environment variables inside the strategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment variable env.coq-version, which uses the globally set coq-version-supported when running the 'supported' case.
80-
- name: Set supported coq-version
81-
if: matrix.coq-version-dummy == 'supported'
82-
run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
8373
- name: Checkout repo
8474
uses: actions/checkout@v4
8575
- name: Build HoTT
8676
uses: coq-community/[email protected]
8777
with:
88-
coq_version: ${{ env.coq-version }}
78+
coq_version: ${{ matrix.coq-version }}
8979
ocaml_version: ${{ env.ocaml-version }}
9080
custom_script: |
9181
startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
@@ -103,29 +93,23 @@ jobs:
10393
strategy:
10494
fail-fast: false
10595
matrix:
106-
# We build on our supported version of coq and the master version
107-
coq-version-dummy:
108-
- 'supported'
109-
- 'latest'
96+
# We build on supported versions; artifacts used for docs and validation
97+
coq-version:
98+
- '9.0'
99+
- '9.1'
110100
include:
111-
- coq-version-dummy: 'dev'
112-
extra-gh-reportify: '--warnings'
113-
env:
114-
coq-version: ${{ matrix.coq-version-dummy }}
101+
- coq-version: 'dev'
102+
extra-gh-reportify: '--warnings'
115103
runs-on: ubuntu-latest
116104
steps:
117-
# Github actions doesn't let us set workflow level environment variables inside the strategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment variable env.coq-version, which uses the globally set coq-version-supported when running the 'supported' case.
118-
- name: Set supported coq-version
119-
if: matrix.coq-version-dummy == 'supported'
120-
run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
121105
# Checkout branch
122106
- uses: actions/checkout@v4
123107
with:
124108
submodules: recursive
125109
# We use the coq docker so we don't have to build coq
126110
- uses: coq-community/[email protected]
127111
with:
128-
coq_version: ${{ env.coq-version }}
112+
coq_version: ${{ matrix.coq-version }}
129113
ocaml_version: ${{ env.ocaml-version }}
130114
custom_script: |
131115
startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
@@ -147,7 +131,7 @@ jobs:
147131
- name: 'Upload Artifact'
148132
uses: actions/upload-artifact@v4
149133
with:
150-
name: workspace-${{ env.coq-version }}
134+
name: workspace-${{ matrix.coq-version }}
151135
path: workspace.tar
152136

153137
# Nix build
@@ -282,7 +266,7 @@ jobs:
282266
mv HoTT.svg HoTTCore.svg dep-graphs/
283267
284268
## Install coq-dpdgraph
285-
opam install coq-dpdgraph.1.0+8.19 -y
269+
opam install coq-dpdgraph -y
286270
287271
# For some reason, we get a stackoverflow. So we are lax
288272
# with making these.
@@ -412,33 +396,26 @@ jobs:
412396
strategy:
413397
fail-fast: false
414398
matrix:
415-
# We build on our supported version of coq and the master version
416-
coq-version-dummy:
417-
- 'supported'
418-
- 'latest'
419-
- 'dev'
420-
env:
421-
coq-version: ${{ matrix.coq-version-dummy }}
399+
coq-version:
400+
- '9.0'
401+
- '9.1'
402+
- 'dev'
422403
runs-on: ubuntu-latest
423404
steps:
424-
# Github actions doesn't let us set workflow level environment variables inside the strategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment variable env.coq-version, which uses the globally set coq-version-supported when running the 'supported' case.
425-
- name: Set supported coq-version
426-
if: matrix.coq-version-dummy == 'supported'
427-
run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
428405
# Checkout branch
429406
- uses: actions/checkout@v4
430407
with:
431408
submodules: recursive
432409
# Download artifact
433410
- uses: actions/download-artifact@v4
434411
with:
435-
name: workspace-${{ env.coq-version }}
412+
name: workspace-${{ matrix.coq-version }}
436413
# Unpack Tar
437414
- run: tar -xf workspace.tar
438415
# We use the coq docker so we don't have to build coq
439416
- uses: coq-community/[email protected]
440417
with:
441-
coq_version: ${{ env.coq-version }}
418+
coq_version: ${{ matrix.coq-version }}
442419
ocaml_version: ${{ env.ocaml-version }}
443420
custom_script: |
444421
startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
@@ -457,33 +434,26 @@ jobs:
457434
strategy:
458435
fail-fast: false
459436
matrix:
460-
# We build on our supported version of coq and the master version
461-
coq-version-dummy:
462-
- 'supported'
463-
- 'latest'
464-
- 'dev'
465-
env:
466-
coq-version: ${{ matrix.coq-version-dummy }}
437+
coq-version:
438+
- '9.0'
439+
- '9.1'
440+
- 'dev'
467441
runs-on: ubuntu-latest
468442
steps:
469-
# Github actions doesn't let us set workflow level environment variables inside the strategy of a job. Therefore we use the dummy variable coq-version in the matrix to set an environment variable env.coq-version, which uses the globally set coq-version-supported when running the 'supported' case.
470-
- name: Set supported coq-version
471-
if: matrix.coq-version-dummy == 'supported'
472-
run: echo "coq-version=${{ env.coq-version-supported }}" >> $GITHUB_ENV
473443
# Checkout branch
474444
- uses: actions/checkout@v4
475445
with:
476446
submodules: recursive
477447
# Download artifact
478448
- uses: actions/download-artifact@v4
479449
with:
480-
name: workspace-${{ env.coq-version }}
450+
name: workspace-${{ matrix.coq-version }}
481451
# Unpack Tar
482452
- run: tar -xf workspace.tar
483453
# We use the coq docker so we don't have to build coq
484454
- uses: coq-community/[email protected]
485455
with:
486-
coq_version: ${{ env.coq-version }}
456+
coq_version: ${{ matrix.coq-version }}
487457
ocaml_version: ${{ env.ocaml-version }}
488458
custom_script: |
489459
startGroup "Workaround permission issue" # https://github.com/coq-community/docker-coq-action#permissions
@@ -492,7 +462,7 @@ jobs:
492462
echo "::remove-matcher owner=coq-problem-matcher::" # remove problem matcher installed by Coq docker action, so we don't get duplicate warning annotations
493463
## Test install target
494464
make install
495-
echo 'Require Import HoTT.HoTT.' | coqtop -q
465+
echo 'Require Import HoTT.HoTT.' | rocq repl -q
496466
497467
- name: Revert permissions
498468
# to avoid a warning at cleanup time - https://github.com/coq-community/docker-coq-action#permissions
@@ -573,10 +543,10 @@ jobs:
573543
# Delete workspace artifacts
574544
- uses: geekyeggo/delete-artifact@v5
575545
with:
576-
name: workspace-${{ env.coq-version-supported }}
546+
name: workspace-9.0
577547
- uses: geekyeggo/delete-artifact@v5
578548
with:
579-
name: workspace-latest
549+
name: workspace-9.1
580550
- uses: geekyeggo/delete-artifact@v5
581551
with:
582552
name: workspace-dev

‎Makefile‎

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -12,7 +12,7 @@ Makefile.coq: Makefile _CoqProject
1212
# Generate _CoqProject file
1313
bash etc/generate_coqproject.sh
1414
# Generate Makefile
15-
$(COQBIN)coq_makefile -f _CoqProject -o Makefile.coq
15+
$(COQBIN)rocq makefile -f _CoqProject -o Makefile.coq
1616

1717
# We replace the html target with real-html, because we want to make
1818
# the timestamp file. We use patsubst rather than subst to do this so

‎theories/Basics/Settings.v‎

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -5,9 +5,9 @@
55
(** ** Plugins *)
66

77
(** Load the Ltac plugin. This is the tactic language we use for proofs. *)
8-
Declare ML Module "ltac_plugin:coq-core.plugins.ltac".
8+
Declare ML Module "ltac_plugin:rocq-runtime.plugins.ltac".
99
(** Load the number string notation plugin. Allowing us to write numbers like [1234]. *)
10-
Declare ML Module "number_string_notation_plugin:coq-core.plugins.number_string_notation".
10+
Declare ML Module "number_string_notation_plugin:rocq-runtime.plugins.number_string_notation".
1111

1212
(** ** Proofs *)
1313

0 commit comments

Comments
 (0)