From 3f19f28aa442763707d076d0386a92d6fcecd64a Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 13 Jan 2026 10:41:56 +0100 Subject: [PATCH 1/2] Only require boot (not entire ssreflect) --- README.md | 2 +- coq-mathcomp-bigenough.opam | 3 ++- meta.yml | 4 ++-- 3 files changed, 5 insertions(+), 4 deletions(-) diff --git a/README.md b/README.md index fa89449..bb7599c 100644 --- a/README.md +++ b/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 diff --git a/coq-mathcomp-bigenough.opam b/coq-mathcomp-bigenough.opam index 69aac11..02c65c3 100644 --- a/coq-mathcomp-bigenough.opam +++ b/coq-mathcomp-bigenough.opam @@ -22,7 +22,8 @@ build: [make "-j%{jobs}%"] install: [make "install"] depends: [ "coq" {(>= "8.10" & < "9.1~") | (= "dev")} - "coq-mathcomp-ssreflect" {>= "1.6"} + ("coq-mathcomp-ssreflect" {>= "1.6" & <= "2.4"} + |"coq-mathcomp-boot" {>= "2.5"}) ] tags: [ diff --git a/meta.yml b/meta.yml index 1afb2fe..dc28582 100644 --- a/meta.yml +++ b/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. --- From 2be1d49e829f6d49689813486136731ab4aeee29 Mon Sep 17 00:00:00 2001 From: Pierre Roux Date: Tue, 13 Jan 2026 10:34:36 +0100 Subject: [PATCH 2/2] Compat with Rocq (without coq shim) --- .github/workflows/docker-action.yml | 2 +- Makefile.common | 8 +++--- coq-mathcomp-bigenough.opam | 22 +++------------- rocq-mathcomp-bigenough.opam | 39 +++++++++++++++++++++++++++++ 4 files changed, 47 insertions(+), 24 deletions(-) create mode 100644 rocq-mathcomp-bigenough.opam diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index fa046ae..21ad485 100644 --- a/.github/workflows/docker-action.yml +++ b/.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: diff --git a/Makefile.common b/Makefile.common index d2a37b1..7e54891 100644 --- a/Makefile.common +++ b/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:: diff --git a/coq-mathcomp-bigenough.opam b/coq-mathcomp-bigenough.opam index 02c65c3..c97941b 100644 --- a/coq-mathcomp-bigenough.opam +++ b/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 " version: "dev" @@ -10,22 +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" & <= "2.4"} - |"coq-mathcomp-boot" {>= "2.5"}) -] - +depends: [ "rocq-mathcomp-bigenough" { = version } ] tags: [ "keyword:bigenough" "keyword:asymptotic reasonning" @@ -36,3 +18,5 @@ tags: [ authors: [ "Cyril Cohen" ] + +synopsis: "Compatibility package for rocq-mathcomp-bigenough" diff --git a/rocq-mathcomp-bigenough.opam b/rocq-mathcomp-bigenough.opam new file mode 100644 index 0000000..6f88c55 --- /dev/null +++ b/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 " +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" +]