From cd4512cd961baac0863f331890a02bef349815e1 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 4 Nov 2025 14:48:58 +0100 Subject: [PATCH 1/2] Adapt to math-comp/math-comp#1433 --- theories/cauchyreals.v | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/theories/cauchyreals.v b/theories/cauchyreals.v index 7229b97..b919860 100644 --- a/theories/cauchyreals.v +++ b/theories/cauchyreals.v @@ -856,9 +856,8 @@ Notation "- x" := (opp_creal x) : creal_scope. Lemma add_crealP (x y : creal) : creal_axiom (fun i => x i + y i). Proof. -exists_big_modulus m F. - move=> e i j he hi hj; rewrite opprD addrAC addrA -addrA [- _ + _]addrC. - by rewrite split_norm_add ?cauchymodP ?divrn_gt0. +exists_big_modulus m F => [e i j he hi hj|]. + by rewrite opprD addrACA split_norm_add ?cauchymodP ?divrn_gt0. by close. Qed. Definition add_creal (x y : creal) := CReal (add_crealP x y). From cf4759761b140d54b55b00b6d104294f886b8518 Mon Sep 17 00:00:00 2001 From: Kazuhiko Sakaguchi Date: Tue, 4 Nov 2025 15:13:11 +0100 Subject: [PATCH 2/2] Update meta.yml --- .github/workflows/docker-action.yml | 3 +-- README.md | 12 ++++++------ coq-mathcomp-real-closed.opam | 8 ++++---- meta.yml | 22 ++++++++++------------ 4 files changed, 21 insertions(+), 24 deletions(-) diff --git a/.github/workflows/docker-action.yml b/.github/workflows/docker-action.yml index 669a9ba..354b711 100644 --- a/.github/workflows/docker-action.yml +++ b/.github/workflows/docker-action.yml @@ -18,8 +18,7 @@ jobs: matrix: image: - 'mathcomp/mathcomp:2.4.0-rocq-prover-9.0' - - 'mathcomp/mathcomp:2.4.0-coq-dev' - - 'mathcomp/mathcomp-dev:coq-dev' + - 'mathcomp/mathcomp-dev:rocq-prover-dev' fail-fast: false steps: - uses: actions/checkout@v4 diff --git a/README.md b/README.md index ce2ed0e..76fc4d0 100644 --- a/README.md +++ b/README.md @@ -24,13 +24,13 @@ order theory of real closed field, through quantifier elimination. - Cyril Cohen (initial) - Assia Mahboubi (initial) - License: [CeCILL-B](CECILL-B) -- Compatible Coq versions: Coq 9.0 or later +- Compatible Rocq/Coq versions: Rocq 9.0 or later - Additional dependencies: - - [MathComp ssreflect 2.3 or later](https://math-comp.github.io) + - [MathComp ssreflect 2.4 or later](https://math-comp.github.io) - [MathComp algebra](https://math-comp.github.io) - [MathComp field](https://math-comp.github.io) - [MathComp bigenough 1.0.0 or later](https://github.com/math-comp/bigenough) -- Coq namespace: `mathcomp.real_closed` +- Rocq/Coq namespace: `mathcomp.real_closed` - Related publication(s): - [Formal proofs in real algebraic geometry: from ordered fields to quantifier elimination](https://hal.inria.fr/inria-00593738v4) doi:[10.2168/LMCS-8(1:2)2012](https://doi.org/10.2168/LMCS-8(1:2)2012) - [Construction of real algebraic numbers in Coq](https://hal.inria.fr/hal-00671809v2) doi:[10.1007/978-3-642-32347-8_6](https://doi.org/10.1007/978-3-642-32347-8_6) @@ -66,7 +66,7 @@ The repository contains Except for the end-results listed above, one should not rely on anything. 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. +library for the [Rocq](https://rocq-prover.org/) prover. ## Development instructions @@ -104,14 +104,14 @@ library for the [Coq](https://coq.inria.fr) proof assistant. 3. You are now in the correct work environment. You can do > make - and do whatever you are accustomed to do with Coq. + and do whatever you are accustomed to do with Rocq. 4. In particular, you can edit files using `emacs` or `coqide`. - If you were already using emacs with proof general, make sure you empty your `coq-prog-name` variables and any other proof general options that used to be tied to a previous local installation of - Coq. + Rocq. - If you do not have emacs installed, but want to use it, you can go back to step 2. and call `nix-shell` with the following option > nix-shell --arg withEmacs true diff --git a/coq-mathcomp-real-closed.opam b/coq-mathcomp-real-closed.opam index b5e77be..f0f16b1 100644 --- a/coq-mathcomp-real-closed.opam +++ b/coq-mathcomp-real-closed.opam @@ -21,10 +21,10 @@ order theory of real closed field, through quantifier elimination.""" build: [make "-j%{jobs}%"] install: [make "install"] depends: [ - "rocq-core" { (>= "9.0" & < "9.2~") | (= "dev") } - "coq-mathcomp-ssreflect" {>= "2.3"} - "coq-mathcomp-algebra" - "coq-mathcomp-field" + "rocq-core" {>= "9.0"} + "rocq-mathcomp-ssreflect" {>= "2.4"} + "rocq-mathcomp-algebra" + "rocq-mathcomp-field" "coq-mathcomp-bigenough" {>= "1.0.0"} ] diff --git a/meta.yml b/meta.yml index afac66f..7606c9f 100644 --- a/meta.yml +++ b/meta.yml @@ -39,29 +39,27 @@ license: file: CECILL-B supported_coq_versions: - text: Coq 9.0 or later + text: Rocq 9.0 or later opam: '{>= "9.0"}' tested_coq_opam_versions: - version: '2.4.0-rocq-prover-9.0' repo: 'mathcomp/mathcomp' -- version: '2.4.0-coq-dev' - repo: 'mathcomp/mathcomp' -- version: 'coq-dev' +- version: 'rocq-prover-dev' repo: 'mathcomp/mathcomp-dev' dependencies: - opam: - name: coq-mathcomp-ssreflect - version: '{>= "2.3"}' + name: rocq-mathcomp-ssreflect + version: '{>= "2.4"}' description: |- - [MathComp ssreflect 2.3 or later](https://math-comp.github.io) + [MathComp ssreflect 2.4 or later](https://math-comp.github.io) - opam: - name: coq-mathcomp-algebra + name: rocq-mathcomp-algebra description: |- [MathComp algebra](https://math-comp.github.io) - opam: - name: coq-mathcomp-field + name: rocq-mathcomp-field description: |- [MathComp field](https://math-comp.github.io) - opam: @@ -87,7 +85,7 @@ documentation: |- Except for the end-results listed above, one should not rely on anything. 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. + library for the [Rocq](https://rocq-prover.org/) prover. ## Development instructions @@ -125,14 +123,14 @@ documentation: |- 3. You are now in the correct work environment. You can do > make - and do whatever you are accustomed to do with Coq. + and do whatever you are accustomed to do with Rocq. 4. In particular, you can edit files using `emacs` or `coqide`. - If you were already using emacs with proof general, make sure you empty your `coq-prog-name` variables and any other proof general options that used to be tied to a previous local installation of - Coq. + Rocq. - If you do not have emacs installed, but want to use it, you can go back to step 2. and call `nix-shell` with the following option > nix-shell --arg withEmacs true