Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Drop support for Coq 8.15 #384

Merged
merged 1 commit into from
Sep 7, 2023
Merged

Drop support for Coq 8.15 #384

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 0 additions & 1 deletion .github/workflows/main.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,6 @@ jobs:
fail-fast: false
matrix:
coq_version:
- '8.15'
- '8.16'
- '8.17'
steps:
Expand Down
670 changes: 0 additions & 670 deletions .github/workflows/nix-action-coq-8.15.yml
View file
Open in desktop

This file was deleted.

8 changes: 0 additions & 8 deletions .nix/config.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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 = {};
Expand Down
2 changes: 0 additions & 2 deletions HB/common/compat_815.elpi
View file
Open in desktop

This file was deleted.

2 changes: 0 additions & 2 deletions HB/common/compat_all.elpi
View file
Open in desktop

This file was deleted.

2 changes: 1 addition & 1 deletion HB/common/log.elpi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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),
Expand Down
2 changes: 1 addition & 1 deletion coq-hierarchy-builder.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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: """
Expand Down
36 changes: 0 additions & 36 deletions structures.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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] :- !,
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand All @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand All @@ -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".
Expand Down Expand Up @@ -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".
Expand All @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down Expand Up @@ -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".
Expand Down
149 changes: 0 additions & 149 deletions tests/about.v.out.15
View file
Open in desktop

This file was deleted.

21 changes: 0 additions & 21 deletions tests/compress_coe.v.out.15
View file
Open in desktop

This file was deleted.

12 changes: 0 additions & 12 deletions tests/hnf.v.out.15
View file
Open in desktop

This file was deleted.