Merge pull request #69 from proux01/no-stdlib

Remove Stdlib dependency

.github/workflows/docker-action.yml

@@ -17,17 +17,13 @@ jobs:
     strategy:
       matrix:
         image:
-          - 'mathcomp/mathcomp:2.1.0-coq-8.17'
           - 'mathcomp/mathcomp:2.1.0-coq-8.18'
-          - '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.3.0-coq-8.19'
           - 'mathcomp/mathcomp:2.3.0-coq-8.20'
-          - 'mathcomp/mathcomp:2.3.0-coq-dev'
-          - 'mathcomp/mathcomp-dev:coq-8.18'
           - 'mathcomp/mathcomp-dev:coq-8.19'
-          - 'mathcomp/mathcomp-dev:coq-dev'
+          - 'mathcomp/mathcomp-dev:coq-8.20'
       fail-fast: false
     steps:
       - uses: actions/checkout@v4

.nix/config.nix

@@ -48,33 +48,44 @@
       multinomials.override.version = "master";
       mathcomp-abel.override.version = "master";
     }; in {
-  "8.17".coqPackages = common-bundles // {
-    coq.override.version = "8.17";
-    mathcomp.override.version = "2.1.0";
-  };
   "8.18".coqPackages = common-bundles // {
     coq.override.version = "8.18";
-    mathcomp.override.version = "2.3.0";
+    coqeal.job = false;
+    mathcomp-apery.job = false;
   };
   "8.19".coqPackages = common-bundles // {
     coq.override.version = "8.19";
-    mathcomp.override.version = "2.3.0";
+    coqeal.job = false;
+    mathcomp-apery.job = false;
   };
   "8.20".coqPackages = common-bundles // {
     coq.override.version = "8.20";
+    coq-elpi.override.version = "2.5.0";
+    coq-elpi.override.elpi-version = "2.0.7";
+    hierarchy-builder.override.version = "1.8.1";
+    mathcomp.override.version = "2.3.0";
+  };
+  "9.0".coqPackages = common-bundles // {
+    coq.override.version = "9.0";
+    coq-elpi.job = true;
+    hierarchy-builder.job = true;
     mathcomp.override.version = "2.3.0";
   };
-  "master".coqPackages = common-bundles // {
+  "master" = { rocqPackages = {
+    rocq-core.override.version = "master";
+    stdlib.override.version = "master";
+    bignums.override.version = "master";
+    rocq-elpi.override.version = "master";
+    rocq-elpi.override.elpi-version = "2.0.7";
+  }; coqPackages = common-bundles // {
     coq.override.version = "master";
+    stdlib.override.version = "master";
     bignums.override.version = "master";
-    paramcoq.override.version = "master";
     coq-elpi.override.version = "master";
+    coq-elpi.override.elpi-version = "2.0.7";
     hierarchy-builder.override.version = "master";
     mathcomp.override.version = "master";
-  };
-  "master".ocamlPackages = {
-    elpi.override.version = "1.19.2";
-  };
+  }; };
   };
 
   ## Cachix caches to use in CI

.nix/coq-nix-toolbox.nix

@@ -1 +1 @@
-"858ff8dd010deded3b9cab8e04fbfad20151af5c"
+"23abc2d7903983f4fd414288677d6b421d412cd6"

Makefile.coq.local

@@ -0,0 +1,8 @@
+pre-all::
+	if command -v coqc > /dev/null && (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
+	  for f in $(shell grep "From Corelib" $$(find . -name "*.v") | cut -d: -f1) ; do \
+	     sed -i.bak $${f} -e 's/From Corelib/From Coq/' ; \
+	     sed -i.bak $${f} -e 's/PosDef/PArith/' ; \
+	     $(RM) $${f}.bak ; \
+	  done ; \
+	fi

README.md

@@ -24,7 +24,7 @@ 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.17 or later
+- Compatible Coq versions: Coq 8.18 or later
 - Additional dependencies:
   - [MathComp ssreflect 2.1 or later](https://math-comp.github.io)
   - [MathComp algebra](https://math-comp.github.io)

coq-mathcomp-real-closed.opam

@@ -21,7 +21,7 @@ order theory of real closed field, through quantifier elimination."""
 build: [make "-j%{jobs}%"]
 install: [make "install"]
 depends: [
-  "coq" {>= "8.17"}
+  "coq" {>= "8.18"}
   "coq-mathcomp-ssreflect" {>= "2.1"}
   "coq-mathcomp-algebra" 
   "coq-mathcomp-field" 

meta.yml

@@ -39,16 +39,12 @@ license:
   file: CECILL-B
 
 supported_coq_versions:
-  text: Coq 8.17 or later
-  opam: '{>= "8.17"}'
+  text: Coq 8.18 or later
+  opam: '{>= "8.18"}'
 
 tested_coq_opam_versions:
-- version: '2.1.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
 - version: '2.1.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
-- version: '2.2.0-coq-8.17'
-  repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.18'
   repo: 'mathcomp/mathcomp'
 - version: '2.2.0-coq-8.19'

theories/cauchyreals.v

@@ -1,6 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-From Coq Require Setoid.
+From Corelib Require Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq choice.
 From mathcomp Require Import fintype bigop binomial order perm ssralg poly.
 From mathcomp Require Import polydiv ssrnum ssrint rat matrix mxpoly polyXY.

theories/ordered_qelim.v

@@ -1,6 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 From HB Require Import structures.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq div.
 From mathcomp Require Import choice fintype bigop finset order fingroup.

theories/polyrcf.v

@@ -988,9 +988,7 @@ case pr1 : (root p r1); case => hrootsl; last 2 first.
     by case/andP => /itvP->.
   move=> x; rewrite in_cons; have [->|exr1] /= := eqVneq; first by rewrite hr1.
   rewrite -hroot (itv_splitUeq hr1) (negPf exr1) /=.
-  case: (_ \in `]r1, _[); rewrite (orbT, orbF); [by []|].
-  by apply: contraFF (hrootsl x) => ->.
-  (* use // above and remove above line when requiring Coq >= 8.17 *)
+  by case: (_ \in `]r1, _[); rewrite (orbT, orbF).
 - case: hrootsl => r0 /min_roots_on [] // hr0 har0 pr0 hr0r1.
   exists [:: r0, r1 & s]; constructor=> //=; last first.
     rewrite (itvP hr0) /= path_min_sorted //; apply/allP=> y.

theories/qe_rcf.v

@@ -1,6 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 From mathcomp Require Import ssreflect ssrfun ssrbool eqtype ssrnat seq path.
 From mathcomp Require Import div choice fintype finfun bigop order ssralg zmodp.
 From mathcomp Require Import poly polydiv ssrnum ssrint interval matrix polyXY.
@@ -615,8 +615,7 @@ Lemma eval_SeqPInfty e ps k k' :
 Proof.
 elim: ps k k' => [|p ps ihps] k k' Pk /=; first by rewrite Pk.
 set X := lead_coef _; grab_eq k'' X; apply: (eval_LeadCoef k'') => lp {X}.
-rewrite (ihps _ (fun ps => k' (eval e lp :: ps))) => [//|lps].
-by rewrite Pk.  (* use //= above and remove line when using Coq >= 8.17 *)
+by rewrite (ihps _ (fun ps => k' (eval e lp :: ps))).
 Qed.
 
 Arguments eval_SeqPInfty [e ps k].

theories/qe_rcf_th.v

@@ -1,6 +1,6 @@
 (* (c) Copyright 2006-2016 Microsoft Corporation and Inria.                  *)
 (* Distributed under the terms of CeCILL-B.                                  *)
-From Coq Require Import Setoid.
+From Corelib Require Import Setoid.
 From mathcomp Require Import all_ssreflect all_algebra.
 From mathcomp Require Import polyorder polyrcf mxtens.