Compile with rocq without coq shim

.github/workflows/docker-action.yml

@@ -28,7 +28,7 @@ jobs:
       - uses: actions/checkout@v2
       - uses: coq-community/docker-coq-action@v1
         with:
-          opam_file: 'coq-mathcomp-bigenough.opam'
+          opam_file: 'rocq-mathcomp-bigenough.opam'
           custom_image: ${{ matrix.image }}
 
 # See also:

Makefile.common

@@ -6,9 +6,9 @@
 # pre-makefile::, this-clean:: and __always__:: may be extended      #
 # Additionally, the following variables may be customized:           #
 SUBDIRS?=
-COQBIN?=$(dir $(shell which coqtop))
-COQMAKEFILE?=$(COQBIN)coq_makefile
-COQDEP?=$(COQBIN)coqdep
+COQBIN?=$(dir $(shell command -v coqtop || command -v rocq))
+COQMAKEFILE?=$(shell command -v coq_makefile || echo "$(COQBIN)rocq makefile")
+COQDEP?=$(shell command -v coqdep || echo "$(COQBIN)rocq dep")
 COQPROJECT?=_CoqProject
 COQMAKEOPTIONS?=
 COQMAKEFILEOPTIONS?=
@@ -67,7 +67,7 @@ install: __always__ Makefile.coq
 COQFILES := $(shell grep '.v$$' $(COQPROJECT))
 
 count:
-	@coqwc $(COQFILES) | tail -1 | \
+	@rocq wc $(COQFILES) | tail -1 | \
 	  awk '{printf ("%d (spec=%d+proof=%d)\n", $$1+$$2, $$1, $$2)}'
 # Additionally cleaning backup (*~) files ----------------------------
 this-distclean::

README.md

@@ -25,7 +25,7 @@ library.
 - License: [CeCILL-B](LICENSE)
 - Compatible Coq versions: 8.10 or later
 - Additional dependencies:
-  - [MathComp ssreflect](https://math-comp.github.io) 1.6 or later
+  - [MathComp boot](https://math-comp.github.io) 1.6 or later (MathComp ssreflect for versions <= 2.4.0)
 - Coq namespace: `mathcomp.bigenough`
 - Related publication(s): none
 

coq-mathcomp-bigenough.opam

@@ -1,6 +1,3 @@
-# This file was generated from `meta.yml`, please do not edit manually.
-# Follow the instructions on https://github.com/coq-community/templates to regenerate.
-
 opam-version: "2.0"
 maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
 version: "dev"
@@ -10,21 +7,7 @@ dev-repo: "git+https://github.com/math-comp/bigenough.git"
 bug-reports: "https://github.com/math-comp/bigenough/issues"
 license: "CeCILL-B"
 
-synopsis: "A small library to do epsilon - N reasoning"
-description: """
-The package contains a package to reasoning with big enough objects
-(mostly natural numbers). This package is essentially for backward
-compatibility purposes as `bigenough` will be subsumed by the near
-tactics. The formalization is based on the Mathematical Components
-library."""
-
-build: [make "-j%{jobs}%"]
-install: [make "install"]
-depends: [
-  "coq" {(>= "8.10" & < "9.1~") | (= "dev")}
-  "coq-mathcomp-ssreflect" {>= "1.6"}
-]
-
+depends: [ "rocq-mathcomp-bigenough" { = version } ]
 tags: [
   "keyword:bigenough"
   "keyword:asymptotic reasonning"
@@ -35,3 +18,5 @@ tags: [
 authors: [
   "Cyril Cohen"
 ]
+
+synopsis: "Compatibility package for rocq-mathcomp-bigenough"

meta.yml

@@ -42,7 +42,7 @@ dependencies:
     name: coq-mathcomp-ssreflect
     version: '{>= "1.6"}'
   description: |-
-    [MathComp ssreflect](https://math-comp.github.io) 1.6 or later
+    [MathComp boot](https://math-comp.github.io) 1.6 or later (MathComp ssreflect for versions <= 2.4.0)
 
 tested_coq_opam_versions:
 - version: '8.10'
@@ -67,5 +67,5 @@ documentation: |-
   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.
 ---

rocq-mathcomp-bigenough.opam

@@ -0,0 +1,39 @@
+# This file was generated from `meta.yml`, please do not edit manually.
+# Follow the instructions on https://github.com/coq-community/templates to regenerate.
+
+opam-version: "2.0"
+maintainer: "Cyril Cohen <cyril.cohen@inria.fr>"
+version: "dev"
+
+homepage: "https://github.com/math-comp/bigenough"
+dev-repo: "git+https://github.com/math-comp/bigenough.git"
+bug-reports: "https://github.com/math-comp/bigenough/issues"
+license: "CeCILL-B"
+
+synopsis: "A small library to do epsilon - N reasoning"
+description: """
+The package contains a package to reasoning with big enough objects
+(mostly natural numbers). This package is essentially for backward
+compatibility purposes as `bigenough` will be subsumed by the near
+tactics. The formalization is based on the Mathematical Components
+library."""
+
+build: [make "-j%{jobs}%"]
+install: [make "install"]
+depends: [
+  ("coq" {>= "8.10" & < "8.21~"}
+  | "rocq-core" {>= "9.0" | = "dev"})
+  ("coq-mathcomp-ssreflect" {>= "1.6" & <= "2.4"}
+  |"coq-mathcomp-boot" {>= "2.5"})
+]
+
+tags: [
+  "keyword:bigenough"
+  "keyword:asymptotic reasonning"
+  "keyword:small scale reflection"
+  "keyword:mathematical components"
+  "logpath:mathcomp.bigenough"
+]
+authors: [
+  "Cyril Cohen"
+]