Merge pull request #18 from pi8027/meta_yml

Update meta.yml and dependencies

Author: CohenCyril

.github/workflows/docker-action.yml

@@ -9,6 +9,7 @@ on:
   pull_request:
     branches:
       - '**'
+  workflow_dispatch:
 
 jobs:
   build:
@@ -25,12 +26,13 @@ jobs:
           - 'coqorg/coq:dev'
       fail-fast: false
     steps:
-      - uses: actions/checkout@v2
+      - uses: actions/checkout@v4
       - uses: coq-community/docker-coq-action@v1
         with:
           opam_file: 'rocq-mathcomp-bigenough.opam'
           custom_image: ${{ matrix.image }}
 
+
 # See also:
 # https://github.com/coq-community/docker-coq-action#readme
 # https://github.com/erikmd/docker-coq-github-action-demo

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/math-comp/bigenough/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/bigenough/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/math-comp/bigenough/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/bigenough/actions/workflows/docker-action.yml
 
 
 
@@ -23,10 +23,10 @@ library.
 - Author(s):
   - Cyril Cohen
 - License: [CeCILL-B](LICENSE)
-- Compatible Coq versions: 8.10 or later
+- Compatible Rocq/Coq versions: 8.10 or later
 - Additional dependencies:
   - [MathComp boot](https://math-comp.github.io) 1.6 or later (MathComp ssreflect for versions <= 2.4.0)
-- Coq namespace: `mathcomp.bigenough`
+- Rocq/Coq namespace: `mathcomp.bigenough`
 - Related publication(s): none
 
 ## Building and installation instructions
@@ -35,15 +35,19 @@ The easiest way to install the latest released version of bigenough
 is via [OPAM](https://opam.ocaml.org/doc/Install.html):
 
 ```shell
-opam repo add coq-released https://coq.inria.fr/opam/released
-opam install coq-mathcomp-bigenough
+opam repo add rocq-released https://rocq-prover.org/opam/released
+opam install rocq-mathcomp-bigenough
 ```
 
-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/math-comp/bigenough.git
 cd bigenough
+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
 ```
@@ -55,4 +59,4 @@ This repository is essentially for archiving purposes as `bigenough`
 will be subsumed by the [near tactics](https://github.com/math-comp/analysis/blob/9bfd5a1971c6989f51d9c44341bb71b2fd5e3c76/topology.v#L93).
 
 The formalization is based on the [Mathematical Components](https://github.com/math-comp/math-comp) library for the [Coq](https://coq.inria.fr) proof assistant,
-although it requires only the ssreflect package.
+although it requires only the boot package.

meta.yml

@@ -1,7 +1,7 @@
 ---
 fullname: bigenough
 shortname: bigenough
-opam_name: coq-mathcomp-bigenough
+opam_name: rocq-mathcomp-bigenough
 organization: math-comp
 community: false
 action: true

rocq-mathcomp-bigenough.opam

@@ -22,9 +22,9 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   ("coq" {>= "8.10" & < "8.21~"}
-  | "rocq-core" {>= "9.0" | = "dev"})
+  | "rocq-core" {>= "9.0"})
   ("coq-mathcomp-ssreflect" {>= "1.6" & <= "2.4"}
-  |"coq-mathcomp-boot" {>= "2.5"})
+  |"rocq-mathcomp-boot" {>= "2.5"})
 ]
 
 tags: [