Merge pull request #100 from coq-community/use-rocq-prover

feat: Use `rocq/rocq-prover` namespace when needed
coq-community · Feb 5, 2025 · 09f3065 · 09f3065
2 parents ae62702 + 93d8344
commit 09f3065
Show file tree

Hide file tree

Showing 3 changed files with 52 additions and 30 deletions.
diff --git a/.github/workflows/coq-demo.yml b/.github/workflows/coq-demo.yml
@@ -25,7 +25,7 @@ jobs:
         # To get the list of supported (coq, ocaml) versions from coqorg/coq,
         # see https://github.com/coq-community/docker-coq/wiki#supported-tags
         coq_version:
-          - '8.18'
+          - '8.20'
           - 'latest-native'
           - 'dev'
         ocaml_version: ['default']
@@ -58,7 +58,7 @@ jobs:
       matrix:
         image:
           - 'mathcomp/mathcomp-dev:coq-dev'
-          - 'mathcomp/mathcomp:latest-coq-8.19'
+          - 'mathcomp/mathcomp:latest-coq-8.20'
           # - 'mathcomp/mathcomp:latest-coq-dev'  # not always available,
           # see https://hub.docker.com/r/mathcomp/mathcomp#supported-tags
       fail-fast: false  # don't stop jobs if one fails
@@ -92,8 +92,10 @@ jobs:
     strategy:
       matrix:
         image:
+          # TODO: Update as soon as Rocq 9.0.0 goes live
           - 'coqorg/coq:latest'
-          - 'coqorg/coq:dev'
+          - 'rocq/rocq-prover:9.0'
+          - 'rocq/rocq-prover:dev'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       ################################################################
@@ -121,7 +123,7 @@ jobs:
             endGroup
           before_script: |
             startGroup "Workaround permission issue"
-              sudo chown -R coq:coq .
+              sudo chown -R 1000:1000 .
             endGroup
           script: |
             startGroup "Build project"
@@ -150,7 +152,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:latest'
-          - 'coqorg/coq:dev'
+          - 'rocq/rocq-prover:9.0'
+          - 'rocq/rocq-prover:dev'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       ################################################################
@@ -182,7 +185,7 @@ jobs:
               opam list
             endGroup
             startGroup "Workaround permission issue"
-              sudo chown -R coq:coq .
+              sudo chown -R 1000:1000 .
             endGroup
             startGroup "Build project"
               coq_makefile -f _CoqProject -o Makefile
@@ -248,7 +251,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'coqorg/coq:dev'
+          - 'rocq/rocq-prover:dev'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       ################################################################
@@ -281,7 +284,8 @@ jobs:
       matrix:
         image:
           - 'coqorg/coq:latest'
-          - 'coqorg/coq:dev'
+          - 'rocq/rocq-prover:9.0'
+          - 'rocq/rocq-prover:dev'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       ################################################################
@@ -348,7 +352,7 @@ jobs:
           custom_image: ${{ matrix.image }}
           before_script: |
             startGroup "Workaround permission issue"
-              sudo chown -R coq:coq .
+              sudo chown -R 1000:1000 .
             endGroup
           script: |
             startGroup "Build project"
@@ -384,7 +388,7 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:latest-coq-8.19'
+          - 'mathcomp/mathcomp:latest-coq-8.20'
       fail-fast: false  # don't stop jobs if one fails
     steps:
       ################################################################

diff --git a/README.md b/README.md
@@ -35,16 +35,19 @@
 [conduct-link]: https://github.com/coq-community/manifesto/blob/master/CODE_OF_CONDUCT.md
 
 This is a GitHub Action that uses (by default)
-[coqorg/coq](https://hub.docker.com/r/coqorg/coq/) Docker images,
-which in turn is based on [coqorg/base](https://hub.docker.com/r/coqorg/base/),
+[rocq/rocq-prover](https://hub.docker.com/r/rocq/rocq-prover/) Docker images
+(for Rocq ≥ 9.0) and
+[coqorg/coq](https://hub.docker.com/r/coqorg/coq/) Docker images
+(for Coq ≤ 8.20.1),
+which in turn are based on [rocq/base](https://hub.docker.com/r/rocq/base/),
 a Docker image with a Debian environment.
 
-|   | GitHub repo                                                             | Type          | Docker Hub                                             |
-|---|-------------------------------------------------------------------------|---------------|--------------------------------------------------------|
-| ⊙ | [docker-coq-action](https://github.com/coq-community/docker-coq-action) | GitHub Action | N/A                                                    |
-| ↳ | [docker-coq](https://github.com/coq-community/docker-coq)               | Dockerfile    | [`coqorg/coq`](https://hub.docker.com/r/coqorg/coq/)   |
-| ↳ | [docker-base](https://github.com/coq-community/docker-base)             | Dockerfile    | [`coqorg/base`](https://hub.docker.com/r/coqorg/base/) |
-| ↳ | Debian                                                                  | Linux distro  | [`debian`](https://hub.docker.com/_/debian/)           |
+|   | GitHub repo                                                             | Type          | Docker Hub                                                       |
+|---|-------------------------------------------------------------------------|---------------|------------------------------------------------------------------|
+| ⊙ | [docker-coq-action](https://github.com/coq-community/docker-coq-action) | GitHub Action | N/A                                                              |
+| ↳ | [docker-rocq](https://github.com/coq-community/docker-rocq)             | Dockerfile    | [`rocq/rocq-prover`](https://hub.docker.com/r/rocq/rocq-prover/) |
+| ↳ | [docker-base](https://github.com/coq-community/docker-base)             | Dockerfile    | [`rocq/base`](https://hub.docker.com/r/rocq/base/)               |
+| ↳ | Debian                                                                  | Linux distro  | [`debian`](https://hub.docker.com/_/debian/)                     |
 
 For more details about these images, see the
 [docker-coq wiki](https://github.com/coq-community/docker-coq/wiki).
@@ -359,7 +362,7 @@ If this variable is unset, its value is computed from the values of
 keywords `coq_version` and `ocaml_version`.
 
 If you use the standard
-[`docker-coq`](https://github.com/coq-community/docker-coq) images, we
+[`docker-rocq`](https://github.com/coq-community/docker-rocq) images, we
 recommend to directly use keywords `coq_version` and `ocaml_version`.
 
 If you use another registry such as that of
@@ -536,7 +539,7 @@ Instead, you should write one of the following variants:
 ### Permissions
 
 If you use the
-[`docker-coq`](https://github.com/coq-community/docker-coq) images,
+[`docker-rocq`](https://github.com/coq-community/docker-rocq) images,
 the container user has UID=GID=1000 while the GitHub Actions workdir
 has (UID=1001, GID=116).
 This is not an issue when relying on `opam` to build the Coq project.
@@ -551,7 +554,7 @@ runs-on: ubuntu-latest
 strategy:
   matrix:
     image:
-      - 'coqorg/coq:dev'
+      - 'rocq/rocq-prover:dev'
   fail-fast: false  # don't stop jobs if one fails
 steps:
   - uses: actions/checkout@v4
@@ -561,7 +564,7 @@ steps:
       custom_image: ${{ matrix.image }}
       before_script: |
         startGroup "Workaround permission issue"
-          sudo chown -R coq:coq .  # <--
+          sudo chown -R 1000:1000 .  # <--
         endGroup
       script: |
         startGroup "Build project"
@@ -610,7 +613,7 @@ runs-on: ubuntu-latest
 strategy:
   matrix:
     image:
-      - 'coqorg/coq:dev'
+      - 'rocq/rocq-prover:dev'
   fail-fast: false  # don't stop jobs if one fails
     steps:
       - uses: coq-community/docker-coq-action@v1
@@ -669,7 +672,7 @@ runs-on: ubuntu-latest
 strategy:
   matrix:
     image:
-      - 'coqorg/coq:latest'
+      - 'rocq/rocq-prover:9.0'
   fail-fast: false  # don't stop jobs if one fails
 steps:
   - uses: actions/checkout@v4
@@ -694,7 +697,7 @@ steps:
 ### Install Debian packages
 
 If you use `docker-coq-action` with a
-[Docker-Coq](https://github.com/coq-community/docker-coq) image (the
+[docker-rocq](https://github.com/coq-community/docker-rocq) image (the
 default when the [`custom_image`](#custom_image) field is omitted),
 the image is based on Debian stable and the container user
 (UID=GID=1000) has `sudo` rights, so you can rely on `apt-get` to
@@ -708,7 +711,7 @@ runs-on: ubuntu-latest
 strategy:
   matrix:
     image:
-      - 'coqorg/coq:dev'
+      - 'rocq/rocq-prover:dev'
   fail-fast: false  # don't stop jobs if one fails
 steps:
   - uses: actions/checkout@v4

diff --git a/entrypoint.sh b/entrypoint.sh
@@ -117,13 +117,28 @@ if test -z "$INPUT_CUSTOM_IMAGE"; then
         exit 1
     fi
 
+    if [ "${INPUT_COQ_VERSION%%-*}" = 'latest' ]; then
+
+        # TODO: Update once 9.0.0 is released
+        ROCQ_PREFIX="coqorg/coq"
+
+    elif [ "${INPUT_COQ_VERSION%%.*}" = '8' ]; then
+
+        ROCQ_PREFIX="coqorg/coq"
+
+    else # e.g. 9 or dev
+
+        ROCQ_PREFIX="rocq/rocq-prover"
+
+    fi
+
     if [ "$INPUT_OCAML_VERSION" = 'default' ]; then
 
-        COQ_IMAGE="coqorg/coq:$INPUT_COQ_VERSION"
+        COQ_IMAGE="$ROCQ_PREFIX:$INPUT_COQ_VERSION"
 
-    elif printf "%s" "$INPUT_COQ_VERSION" | grep -e '.-native$' -q; then
+    elif printf "%s" "$INPUT_COQ_VERSION" | grep -e '.-native' -q; then
 
-        COQ_IMAGE="coqorg/coq:$INPUT_COQ_VERSION"
+        COQ_IMAGE="$ROCQ_PREFIX:$INPUT_COQ_VERSION"
 
         if test -n "$INPUT_OCAML_VERSION"; then
             # HERE, "ocaml_version" is nonempty and different from 'default'
@@ -158,7 +173,7 @@ Error: Setting ocaml_version to "minimal" is NOT SUPPORTED ANYMORE: please use "
 EOF
             exit 1
         else
-            COQ_IMAGE="coqorg/coq:${INPUT_COQ_VERSION}-ocaml-${INPUT_OCAML_VERSION}"
+            COQ_IMAGE="${ROCQ_PREFIX}:${INPUT_COQ_VERSION}-ocaml-${INPUT_OCAML_VERSION}"
         fi
     fi
 else