Update CI and README

.github/workflows/docker-action.yml

@@ -19,8 +19,18 @@ jobs:
         image:
           - 'mathcomp/mathcomp:2.0.0-coq-8.16'
           - 'mathcomp/mathcomp:2.0.0-coq-8.17'
-          - 'mathcomp/mathcomp-dev:coq-8.16'
+          - 'mathcomp/mathcomp:2.0.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.1.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.16'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.17'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.18'
+          - 'mathcomp/mathcomp:2.2.0-coq-8.19'
+          - 'mathcomp/mathcomp:2.2.0-coq-dev'
           - 'mathcomp/mathcomp-dev:coq-8.17'
+          - 'mathcomp/mathcomp-dev:coq-8.18'
+          - 'mathcomp/mathcomp-dev:coq-8.19'
           - 'mathcomp/mathcomp-dev:coq-dev'
       fail-fast: false
     steps:

.nix/config.nix

@@ -37,20 +37,43 @@
   ## alternative configuration
   ## When generating GitHub Action CI, one workflow file
   ## will be created per bundle
-  bundles."8.16".coqPackages = {
+  bundles = let
+    common-bundles = {
+      coqeal.override.version = "master";
+      mathcomp-apery.override.version = "master";
+      mathcomp-algebra-tactics.override.version = "master";
+      mathcomp-bigenough.override.version = "master";
+      mathcomp-finmap.override.version = "master";
+      mathcomp-zify.override.version = "master";
+      multinomials.override.version = "master";
+    }; in {
+  "8.16".coqPackages = common-bundles // {
     coq.override.version = "8.16";
     mathcomp.override.version = "2.0.0";
+    multinomials.job = false;  # broken with dune on 8.16 in nixpkgs
+    coqeal.job = false;
+    mathcomp-apery.job = false;
   };
-  bundles."8.17".coqPackages = {
+  "8.17".coqPackages = common-bundles // {
     coq.override.version = "8.17";
-    mathcomp.override.version = "2.0.0";
+    mathcomp.override.version = "2.1.0";
+  };
+  "8.18".coqPackages = common-bundles // {
+    coq.override.version = "8.18";
+    mathcomp.override.version = "2.2.0";
   };
-  bundles."master".coqPackages = {
+  "8.19".coqPackages = common-bundles // {
+    coq.override.version = "8.19";
+    mathcomp.override.version = "2.2.0";
+  };
+  "master".coqPackages = common-bundles // {
     coq.override.version = "master";
+    bignums.override.version = "master";
+    paramcoq.override.version = "master";
     coq-elpi.override.version = "coq-master";
-    hierarchy-builder.override.version = "coq-master";
+    hierarchy-builder.override.version = "master";
     mathcomp.override.version = "master";
-    mathcomp-bigenough.override.version = "1.0.1";
+  };
   };
 
   ## Cachix caches to use in CI

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"575258fdeb76c712740f30f23ccf5ed1918c2332"
+"1cad18e8537b4f6d6ad97d6eb57fa61e3dbcad59"

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/real-closed/workflows/Docker%20CI/badge.svg?branch=master
-[docker-action-link]: https://github.com/math-comp/real-closed/actions?query=workflow:"Docker%20CI"
+[docker-action-shield]: https://github.com/math-comp/real-closed/actions/workflows/docker-action.yml/badge.svg?branch=master
+[docker-action-link]: https://github.com/math-comp/real-closed/actions/workflows/docker-action.yml
 
 
 
@@ -24,11 +24,11 @@ order theory of real closed field, through quantifier elimination.
   - Cyril Cohen (initial)
   - Assia Mahboubi (initial)
 - License: [CeCILL-B](CECILL-B)
-- Compatible Coq versions: Coq 8.13 or later
+- Compatible Coq versions: Coq 8.16 or later
 - Additional dependencies:
-  - [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
-  - [MathComp algebra 1.13 or later](https://math-comp.github.io)
-  - [MathComp field 1.13 or later](https://math-comp.github.io)
+  - [MathComp ssreflect 2.0 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`
 - Related publication(s):

coq-mathcomp-real-closed.opam

@@ -22,9 +22,9 @@ build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
   "coq" {>= "8.16"}
-  "coq-mathcomp-ssreflect" {>= "2.0.0"}
-  "coq-mathcomp-algebra"
-  "coq-mathcomp-field"
+  "coq-mathcomp-ssreflect" {>= "2.0"}
+  "coq-mathcomp-algebra" 
+  "coq-mathcomp-field" 
   "coq-mathcomp-bigenough" {>= "1.0.0"}
 ]
 

meta.yml

@@ -39,53 +39,55 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.13 or later
-  opam: '{>= "8.13"}'
+  text: Coq 8.16 or later
+  opam: '{>= "8.16"}'
 
 tested_coq_opam_versions:
-- version: '1.13.0-coq-8.13'
+- version: '2.0.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.14'
+- version: '2.0.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.13.0-coq-8.15'
+- version: '2.0.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.13'
+- version: '2.1.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.14'
+- version: '2.1.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.14.0-coq-8.15'
+- version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.13'
+- version: '2.2.0-coq-8.16'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.14'
+- version: '2.2.0-coq-8.17'
   repo: 'mathcomp/mathcomp'
-- version: '1.15.0-coq-8.15'
+- version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: 'coq-8.13'
+- version: '2.2.0-coq-8.19'
+  repo: 'mathcomp/mathcomp'
+- version: '2.2.0-coq-dev'
+  repo: 'mathcomp/mathcomp'
+- version: 'coq-8.17'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.14'
+- version: 'coq-8.18'
   repo: 'mathcomp/mathcomp-dev'
-- version: 'coq-8.15'
+- version: 'coq-8.19'
   repo: 'mathcomp/mathcomp-dev'
 - version: 'coq-dev'
   repo: 'mathcomp/mathcomp-dev'
 
 dependencies:
 - opam:
     name: coq-mathcomp-ssreflect
-    version: '{>= "1.13.0"}'
+    version: '{>= "2.0"}'
   description: |-
-    [MathComp ssreflect 1.13 or later](https://math-comp.github.io)
+    [MathComp ssreflect 2.0 or later](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-algebra
-    version: '{>= "1.13.0"}'
   description: |-
-    [MathComp algebra 1.13 or later](https://math-comp.github.io)
+    [MathComp algebra](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-field
-    version: '{>= "1.13.0"}'
   description: |-
-    [MathComp field 1.13 or later](https://math-comp.github.io)
+    [MathComp field](https://math-comp.github.io)
 - opam:
     name: coq-mathcomp-bigenough
     version: '{>= "1.0.0"}'

theories/ordered_qelim.v

@@ -82,16 +82,16 @@
 Bind Scope oterm_scope with term.
 Bind Scope oterm_scope with formula.
 Delimit Scope oterm_scope with oT.
 Arguments Add _ _%oT _%oT.
 Arguments Opp _ _%oT.
 Arguments NatMul _ _%oT _%N.
 Arguments Mul _ _%oT _%oT.
 Arguments Mul _ _%oT _%oT.
 Arguments Inv _ _%oT.
 Arguments Exp _ _%oT _%N.
 Arguments Equal _ _%oT _%oT.
 Arguments Unit _ _%oT.
 Arguments And _ _%oT _%oT.
 Arguments Or _ _%oT _%oT.
 Arguments Implies _ _%oT _%oT.
 Arguments Not _ _%oT.
@@ -172,15 +172,14 @@
 Delimit Scope oclause_scope with OCLAUSE.
 Open Scope oclause_scope.
 
-Notation "p .1" := (@eq_of_oclause _ p)
-  (at level 2, left associativity, format "p .1") : oclause_scope.
-Notation "p .2" := (@neq_of_oclause _ p)
-  (at level 2, left associativity, format "p .2") : oclause_scope.
+(* TODO: add `at level 1, left associativity` when dropping the support for Coq 8.19 *)
+Notation "p .1" := (@eq_of_oclause _ p) (format "p .1") : oclause_scope.
+Notation "p .2" := (@neq_of_oclause _ p) (format "p .2") : oclause_scope.
 
 Notation "p .3" := (@lt_of_oclause _ p)
-  (at level 2, left associativity, format "p .3") : oclause_scope.
+  (at level 1, left associativity, format "p .3") : oclause_scope.
 Notation "p .4" := (@le_of_oclause _ p)
-  (at level 2, left associativity, format "p .4") : oclause_scope.
+  (at level 1, left associativity, format "p .4") : oclause_scope.
 
 Definition oclause_eq (T : eqType)(t1 t2 : oclause T) :=
   let: Oclause eq_l1 neq_l1 lt_l1 leq_l1 := t1 in