diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 130255c..25e9898 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -16,17 +16,19 @@ jobs: runs-on: ubuntu-latest strategy: matrix: - coq_version: - - 'dev' - - '8.19' - - '8.18' + image: + - 'coqorg/coq:8.20' + - 'coqorg/coq:8.19' + - 'coqorg/coq:8.18' + - 'rocq/rocq-prover:dev' + - 'rocq/rocq-prover:9.0' fail-fast: false steps: - uses: actions/checkout@v4 - uses: coq-community/docker-coq-action@v1 with: opam_file: 'coq-math-classes.opam' - coq_version: ${{ matrix.coq_version }} + custom_image: ${{ matrix.image }} before_install: | startGroup "Setup and print opam config" opam repo -a --set-default add coq-extra-dev https://coq.inria.fr/opam/extra-dev diff --git a/README.md b/README.md index 16a4d20..dba32cd 100644 --- a/README.md +++ b/README.md @@ -51,7 +51,7 @@ notations. - Bas Spitters ([**@spitters**](https://github.com/spitters)) - Xia Li-yao ([**@Lysxia**](https://github.com/Lysxia)) - License: [MIT License](LICENSE) -- Compatible Coq versions: Coq 8.18 or later (use releases for other Coq versions) +- Compatible Coq versions: Coq/Rocq 8.18 or later (use releases for other Coq/Rocq versions) - Additional dependencies: - [BigNums](https://github.com/coq/bignums) - Coq namespace: `MathClasses` diff --git a/coq-math-classes.opam b/coq-math-classes.opam index 9c5c029..2dfd230 100644 --- a/coq-math-classes.opam +++ b/coq-math-classes.opam @@ -30,7 +30,7 @@ build: [ ] install: [make "install"] depends: [ - "coq" {(>= "8.18" & < "8.20~") | (= "dev")} + "coq" {(>= "8.18" & < "9.1~") | (= "dev")} "coq-bignums" ] diff --git a/meta.yml b/meta.yml index 80c7b8f..c14301c 100644 --- a/meta.yml +++ b/meta.yml @@ -51,11 +51,15 @@ license: identifier: MIT supported_coq_versions: - text: Coq 8.18 or later (use releases for other Coq versions) - opam: '{(>= "8.18" & < "8.20~") | (= "dev")}' + text: Coq/Rocq 8.18 or later (use releases for other Coq/Rocq versions) + opam: '{(>= "8.18" & < "9.1~") | (= "dev")}' -tested_coq_opam_versions: +tested_rocq_opam_versions: - version: dev +- version: "9.0" + +tested_coq_opam_versions: +- version: "8.20" - version: "8.19" - version: "8.18"