Merge pull request #384 from proux01/drop_coq_815

Drop support for Coq 8.15
math-comp · Sep 7, 2023 · a869fed · a869fed
2 parents 4c7c83d + 16a944a
commit a869fed
Show file tree

Hide file tree

Showing 11 changed files with 2 additions and 903 deletions.
diff --git a/.github/workflows/main.yml b/.github/workflows/main.yml
@@ -17,7 +17,6 @@ jobs:
       fail-fast: false
       matrix:
         coq_version:
-          - '8.15'
           - '8.16'
           - '8.17'
     steps:

diff --git a/.github/workflows/nix-action-coq-8.15.yml b/.github/workflows/nix-action-coq-8.15.yml
diff --git a/.nix/config.nix b/.nix/config.nix
@@ -38,14 +38,6 @@
     "coq-8.16".coqPackages = mcHBcommon // {
       coq.override.version = "8.16";
     };
-
-    "coq-8.15".coqPackages = mcHBcommon // {
-      coq.override.version = "8.15";
-      mathcomp.job = false;
-      mathcomp-classical.job = false;
-      mathcomp-analysis.job = false;
-      mathcomp-infotheo.job = false;
-    };
   };
   cachix.coq = {};
   cachix.coq-community = {};

diff --git a/HB/common/compat_815.elpi b/HB/common/compat_815.elpi
diff --git a/HB/common/compat_all.elpi b/HB/common/compat_all.elpi
diff --git a/HB/common/log.elpi b/HB/common/log.elpi
@@ -159,7 +159,7 @@ env.import-module MPNice M :- std.do! [
 
 pred coercion.declare i:coercion.
 coercion.declare C :- std.do! [
-  compat.coercion.declare C,
+  @global! => @reversible! => coq.coercion.declare C,
   C = coercion GR _ SRCGR TGTCL,
   coq.gref->id GR Name,
   log.private.log-vernac (log.private.coq.vernac.coercion Name SRCGR TGTCL),

diff --git a/coq-hierarchy-builder.opam b/coq-hierarchy-builder.opam
@@ -12,7 +12,7 @@ build: [ [ make "build"]
          [ make "test-suite" ] {with-test}
        ]
 install: [ make "install" ]
-depends: [ "coq-elpi" { (>= "1.14" & < "1.20~") | = "dev" } ]
+depends: [ "coq-elpi" { (>= "1.15" & < "1.20~") | = "dev" } ]
 conflicts: [ "coq-hierarchy-builder-shim" ]
 synopsis: "High level commands to declare and evolve a hierarchy based on packed classes"
 description: """

diff --git a/structures.v b/structures.v
@@ -244,8 +244,6 @@ Elpi Accumulate Db hb.db.
    the commands. To this end, we accumulate the DB first in each command to
    ensure the same dependencies and maximize cache hits. For instance, this
    can save a few (2 or 3) percents of total compilation time on MathComp. *)
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate lp:{{
 
 main [str S] :- !,
@@ -274,8 +272,6 @@ Elpi Export HB.locate.
 
 #[arguments(raw)] Elpi Command HB.about.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -309,8 +305,6 @@ Elpi Export HB.about.
 
 #[arguments(raw)] Elpi Command HB.howto.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -352,8 +346,6 @@ Elpi Export HB.howto.
 
 #[arguments(raw)] Elpi Command HB.status.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -382,8 +374,6 @@ tred file.dot | xdot -
 
 #[arguments(raw)] Elpi Command HB.graph.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -432,8 +422,6 @@ HB.mixin Record MixinName T of Factory1 T & … & FactoryN T := {
 
 #[arguments(raw)] Elpi Command HB.mixin.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -495,8 +483,6 @@ Elpi Export HB.mixin.
 
 Elpi Tactic HB.pack_for.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -519,8 +505,6 @@ Elpi Export HB.pack_for.
 
 Elpi Tactic HB.pack.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -605,8 +589,6 @@ HB.structure Definition StructureName params :=
 
 #[arguments(raw)] Elpi Command HB.structure.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -661,8 +643,6 @@ HB.instance Definition N Params := Factory.Build Params T …
 
 #[arguments(raw)] Elpi Command HB.instance.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -694,8 +674,6 @@ Elpi Export HB.instance.
 
 #[arguments(raw)] Elpi Command HB.factory.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -756,8 +734,6 @@ HB.end.
 
 #[arguments(raw)] Elpi Command HB.builders.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -782,8 +758,6 @@ Elpi Export HB.builders.
 
 #[arguments(raw)] Elpi Command HB.end.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -836,8 +810,6 @@ Export Algebra.Exports.
 
 #[arguments(raw)] Elpi Command HB.export.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -864,8 +836,6 @@ Elpi Export HB.export.
 
 #[arguments(raw)] Elpi Command HB.reexport.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -912,8 +882,6 @@ Notation foo := foo.body.
 
 #[arguments(raw)] Elpi Command HB.lock.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -963,8 +931,6 @@ HB.instance Definition _ : Ml ... T := ml.
 
 #[arguments(raw)] Elpi Command HB.declare.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
@@ -1000,8 +966,6 @@ Elpi Export HB.declare.
 
 #[arguments(raw)] Elpi Command HB.check.
 Elpi Accumulate Db hb.db.
-#[skip="8.15.*"] Elpi Accumulate File "HB/common/compat_all.elpi".
-#[only="8.15.*"] Elpi Accumulate File "HB/common/compat_815.elpi".
 Elpi Accumulate File "HB/common/stdpp.elpi".
 Elpi Accumulate File "HB/common/database.elpi".
 #[skip="8.1[56].*"] Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".

diff --git a/tests/about.v.out.15 b/tests/about.v.out.15
diff --git a/tests/compress_coe.v.out.15 b/tests/compress_coe.v.out.15
diff --git a/tests/hnf.v.out.15 b/tests/hnf.v.out.15