ci: test against latest Coq and Rocq

Signed-off-by: Yishuai Li <yishuai.li@pingcap.com>

Author: liyishuai

.github/workflows/docker-action.yml

@@ -22,10 +22,14 @@ jobs:
           - 'coqorg/coq:8.16'
           - 'coqorg/coq:8.17'
           - 'coqorg/coq:8.18'
-          - 'coqorg/coq:dev'
+          - 'coqorg/coq:8.19'
+          - 'coqorg/coq:8.20'
+          - 'rocq/rocq-prover:9.0'
+          - 'rocq/rocq-prover:9.1'
+          - 'rocq/rocq-prover:dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v3
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'coq-http.opam'

README.md

@@ -6,8 +6,8 @@ Follow the instructions on https://github.com/coq-community/templates to regener
 
 [![Docker CI][docker-action-shield]][docker-action-link]
 
-[docker-action-shield]: https://github.com/liyishuai/coq-http/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/liyishuai/coq-http/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/liyishuai/coq-http/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/liyishuai/coq-http/actions/workflows/docker-action.yml
 
 
 
@@ -17,18 +17,18 @@ HTTP specification in Coq, testable and verifiable
 ## Meta
 
 - Author(s):
-  - Yishuai Li [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0002-5728-5903)
-  - Li-yao Xia [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0003-2673-4400)
-  - Yao Li [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-8720-883X)
+  - Yishuai Li [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0002-5728-5903)
+  - Li-yao Xia [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0003-2673-4400)
+  - Yao Li [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-8720-883X)
   - Azzam Althagafi
-  - Benjamin C. Pierce [<img src="https://zenodo.org/static/img/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-7839-1636)
+  - Benjamin C. Pierce [<img src="https://zenodo.org/static/images/orcid.svg" height="14px" alt="ORCID logo" />](https://orcid.org/0000-0001-7839-1636)
 - License: [Mozilla Public License 2.0](LICENSE)
-- Compatible Coq versions: 8.14 or later
+- Compatible Rocq/Coq versions: 8.14 or later
 - Additional dependencies:
   - [OCamlbuild](https://github.com/ocaml/ocamlbuild)
   - [QuickChick](https://github.com/QuickChick/QuickChick/)
   - [AsyncTest](https://github.com/liyishuai/coq-async-test)
-- Coq namespace: `HTTP`
+- Rocq/Coq namespace: `HTTP`
 - Related publication(s):
   - [From C to Interaction Trees: Specifying, Verifying, and Testing a Networked Server](https://doi.org/10.1145/3293880.3294106) doi:[10.1145/3293880.3294106](https://doi.org/10.1145/3293880.3294106)
   - [Model-Based Testing of Networked Applications](https://doi.org/10.1145/3460319.3464798) doi:[10.1145/3460319.3464798](https://doi.org/10.1145/3460319.3464798)
@@ -41,15 +41,19 @@ The easiest way to install the latest released version of coq-http
 is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
-opam repo add coq-released https://coq.inria.fr/opam/released
+opam repo add rocq-released https://rocq-prover.org/opam/released
 opam install coq-http
 ```
 
-To instead build and install manually, do:
+To instead build and install manually, you need to make sure that all the
+libraries this development depends on are installed.  The easiest way to do that
+is still to rely on opam:
 
 ``` shell
 git clone https://github.com/liyishuai/coq-http.git
 cd coq-http
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install --deps-only .
 make   # or make -j <number-of-cores-on-your-machine> 
 make install
 ```

meta.yml

@@ -49,7 +49,7 @@ keywords:
   - name: extraction
   - name: reactive systems
 namespace: HTTP
-opam-file-maintainer: 'Yishuai Li <liyishuai.lys@alibaba-inc.com>'
+opam-file-maintainer: 'Yishuai Li <yishuai.li@pingcap.com>'
 supported_coq_versions:
   text: 8.14 or later
   opam: '{ >= "8.14~" }'
@@ -59,6 +59,11 @@ tested_coq_opam_versions:
   - version: '8.16'
   - version: '8.17'
   - version: '8.18'
+  - version: '8.19'
+  - version: '8.20'
+tested_rocq_opam_versions:
+  - version: '9.0'
+  - version: '9.1'
   - version: 'dev'
 action_appendix: |2-
             export: 'OPAMWITHTEST'