Skip to content

Commit 9d43c47

Browse files
committed
Update CI for latest templates and test more modern Coq/Rocq versions.
1 parent a2920bf commit 9d43c47

4 files changed

Lines changed: 16 additions & 10 deletions

File tree

.github/workflows/docker-action.yml

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -16,17 +16,19 @@ jobs:
1616
runs-on: ubuntu-latest
1717
strategy:
1818
matrix:
19-
coq_version:
20-
- 'dev'
21-
- '8.19'
22-
- '8.18'
19+
image:
20+
- 'coqorg/coq:8.20'
21+
- 'coqorg/coq:8.19'
22+
- 'coqorg/coq:8.18'
23+
- 'rocq/rocq-prover:dev'
24+
- 'rocq/rocq-prover:9.0'
2325
fail-fast: false
2426
steps:
2527
- uses: actions/checkout@v4
2628
- uses: coq-community/docker-coq-action@v1
2729
with:
2830
opam_file: 'coq-math-classes.opam'
29-
coq_version: ${{ matrix.coq_version }}
31+
custom_image: ${{ matrix.image }}
3032
before_install: |
3133
startGroup "Setup and print opam config"
3234
opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev

README.md

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -51,7 +51,7 @@ notations.
5151
- Bas Spitters ([**@spitters**](https://github.com/spitters))
5252
- Xia Li-yao ([**@Lysxia**](https://github.com/Lysxia))
5353
- License: [MIT License](LICENSE)
54-
- Compatible Coq versions: Coq 8.18 or later (use releases for other Coq versions)
54+
- Compatible Coq versions: Coq/Rocq 8.18 or later (use releases for other Coq/Rocq versions)
5555
- Additional dependencies:
5656
- [BigNums](https://github.com/coq/bignums)
5757
- Coq namespace: `MathClasses`

coq-math-classes.opam

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -30,7 +30,7 @@ build: [
3030
]
3131
install: [make "install"]
3232
depends: [
33-
"coq" {(>= "8.18" & < "8.20~") | (= "dev")}
33+
"coq" {(>= "8.18" & < "9.1~") | (= "dev")}
3434
"coq-bignums"
3535
]
3636

meta.yml

Lines changed: 7 additions & 3 deletions
Original file line numberDiff line numberDiff line change
@@ -51,11 +51,15 @@ license:
5151
identifier: MIT
5252

5353
supported_coq_versions:
54-
text: Coq 8.18 or later (use releases for other Coq versions)
55-
opam: '{(>= "8.18" & < "8.20~") | (= "dev")}'
54+
text: Coq/Rocq 8.18 or later (use releases for other Coq/Rocq versions)
55+
opam: '{(>= "8.18" & < "9.1~") | (= "dev")}'
5656

57-
tested_coq_opam_versions:
57+
tested_rocq_opam_versions:
5858
- version: dev
59+
- version: "9.0"
60+
61+
tested_coq_opam_versions:
62+
- version: "8.20"
5963
- version: "8.19"
6064
- version: "8.18"
6165

0 commit comments

Comments
 (0)