Skip to content

Drop support for 8.18 and 8.19 #538

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

Merged
merged 1 commit into from
May 30, 2025
Merged

Drop support for 8.18 and 8.19 #538

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
2 changes: 0 additions & 2 deletions .github/workflows/main.yml
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -18,8 +18,6 @@ jobs:
fail-fast: false
matrix:
coq_version:
- '8.18'
- '8.19'
- '8.20'
- '9.0'
steps:
Expand Down
2,275 changes: 0 additions & 2,275 deletions .github/workflows/nix-action-coq-8.18.yml
View file
Open in desktop

This file was deleted.

2,715 changes: 0 additions & 2,715 deletions .github/workflows/nix-action-coq-8.19.yml
View file
Open in desktop

This file was deleted.

1,462 changes: 819 additions & 643 deletions .github/workflows/nix-action-coq-8.20.yml
View file
Open in desktop

Large diffs are not rendered by default.

1,365 changes: 769 additions & 596 deletions .github/workflows/nix-action-coq-9.0.yml
View file
Open in desktop

Large diffs are not rendered by default.

1,487 changes: 922 additions & 565 deletions .github/workflows/nix-action-coq-master.yml
View file
Open in desktop

Large diffs are not rendered by default.

23 changes: 9 additions & 14 deletions .nix/config.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1,6 +1,7 @@
{
format = "1.0.0";
attribute = "hierarchy-builder";
no-rocq-yet = true;
default-bundle = "coq-8.20";
bundles = let
mcHBcommon = {
Expand All @@ -23,7 +24,12 @@
mathcomp-zify.override.version = "master";
mathcomp-algebra-tactics.override.version = "master";
mathcomp-word.override.version = "master";
jasmin.override.version = "main";
coquelicot.override.version = "master";
ExtLib.override.version = "master";
simple-io.override.version = "master";
QuickChick.override.version = "master";
# jasmin.override.version = "main";
jasmin.job = false; # currently broken
};
in {
"coq-master" = { rocqPackages = {
Expand All @@ -38,6 +44,7 @@
coq-elpi.override.version = "master";
coq-elpi.override.elpi-version = "2.0.7";
bignums.override.version = "master";
coquelicot.job = false;
}; };

"coq-9.0".coqPackages = mcHBcommon // {
Expand All @@ -50,19 +57,7 @@
coq.override.version = "8.20";
coq-elpi.override.version = "master";
coq-elpi.override.elpi-version = "2.0.7";
};

"coq-8.19".coqPackages = mcHBcommon // {
coq.override.version = "8.19";
coqeal.job = false; # requries Coq >= 8.20 through coq-elpi master
};

"coq-8.18".coqPackages = mcHBcommon // {
coq.override.version = "8.18";
mathcomp-classical.job = false; # Analysis master dropped suppor for 8.18
mathcomp-analysis.job = false;
coqeal.job = false; # requries Coq >= 8.20 through coq-elpi master
jasmin.job = false;
interval.override.version = "master";
};

};
Expand Down
2 changes: 1 addition & 1 deletion .nix/coq-nix-toolbox.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
@@ -1 +1 @@
"60657f676e682de3e6a2f5d553aa737bf6801efd"
"e88c86a9e0099f95e9b4d2511536e5f3c93a7daa"
2 changes: 2 additions & 0 deletions Changelog.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2,6 +2,8 @@

## Unreleased

Drop compatibility with 8.18 and 8.19

## [1.9.0] - 2025-04-15

Compatible with
Expand Down
8 changes: 0 additions & 8 deletions HB/common/compat_add_secvar_18_19.elpi
View file
Open in desktop

This file was deleted.

51 changes: 17 additions & 34 deletions HB/structures.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -21,18 +21,18 @@
Register id_phant_disabled as hb.id_disabled.
Register ignore as hb.ignore.
Register ignore_disabled as hb.ignore_disabled.
Register Coq.Init.Datatypes.None as hb.none.

Check warning on line 24 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.Init.Datatypes.None has been replaced by
Register nomsg as hb.nomsg.
Register is_not_canonically_a as hb.not_a_msg.
Register Coq.Init.Datatypes.Some as hb.some.

Check warning on line 27 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.Init.Datatypes.Some has been replaced by
Register Coq.Init.Datatypes.pair as hb.pair.

Check warning on line 28 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.Init.Datatypes.pair has been replaced by
Register Coq.Init.Datatypes.prod as hb.prod.

Check warning on line 29 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.Init.Datatypes.prod has been replaced by
Register Coq.Init.Specif.sigT as hb.sigT.

Check warning on line 30 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.Init.Specif.sigT has been replaced by Corelib.Init.Specif.sigT.
Register Coq.ssr.ssreflect.phant as hb.phant.

Check warning on line 31 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.ssr.ssreflect.phant has been replaced by
Register Coq.ssr.ssreflect.Phant as hb.Phant.

Check warning on line 32 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.ssr.ssreflect.Phant has been replaced by
Register Coq.ssr.ssreflect.phantom as hb.phantom.

Check warning on line 33 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.ssr.ssreflect.phantom has been replaced by
Register Coq.ssr.ssreflect.Phantom as hb.Phantom.

Check warning on line 34 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.ssr.ssreflect.Phantom has been replaced by
Register Coq.Init.Logic.eq as hb.eq.

Check warning on line 35 in HB/structures.v

View workflow job for this annotation

GitHub Actions / opam (9.0) 

Coq.Init.Logic.eq has been replaced by Corelib.Init.Logic.eq.
Register Coq.Init.Logic.eq_refl as hb.erefl.
Register new as hb.new.
Register eta as hb.eta.
Expand Down Expand Up @@ -301,8 +301,7 @@
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Elpi Accumulate File "HB/common/log.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/about.elpi".
Elpi Accumulate lp:{{

Expand Down Expand Up @@ -334,8 +333,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/about.elpi".
Expand Down Expand Up @@ -378,8 +376,7 @@
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
Elpi Accumulate File "HB/common/log.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/status.elpi".
Elpi Accumulate lp:{{
Expand Down Expand Up @@ -408,8 +405,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/graph.elpi".
Expand Down Expand Up @@ -458,8 +454,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -541,8 +536,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand All @@ -565,8 +559,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -642,8 +635,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -726,8 +718,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -777,8 +768,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -820,8 +810,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -904,8 +893,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -946,8 +934,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -1021,8 +1008,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/export.elpi".
Expand Down Expand Up @@ -1068,8 +1054,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/export.elpi".
Expand Down Expand Up @@ -1152,8 +1137,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate File "HB/common/synthesis.elpi".
Expand Down Expand Up @@ -1189,8 +1173,7 @@
Elpi Accumulate File "HB/common/stdpp.elpi".
Elpi Accumulate File "HB/common/database.elpi".
Elpi Accumulate File "HB/common/compat_acc_clauses_all.elpi".
#[skip="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
#[only="8.1[89].*"] Elpi Accumulate File "HB/common/compat_add_secvar_18_19.elpi".
Elpi Accumulate File "HB/common/compat_add_secvar_all.elpi".
Elpi Accumulate File "HB/common/utils.elpi".
Elpi Accumulate File "HB/common/log.elpi".
Elpi Accumulate lp:{{
Expand Down
2 changes: 1 addition & 1 deletion Makefile
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -106,7 +106,7 @@ this-config:: __always__
else\
coqc --print-version > config.stamp;\
echo 'configuring for ' `coqc --print-version`;\
if (coqc --version | grep -q '8.18\|8.19\|8.20') ; then \
if (coqc --version | grep -q '8.20') ; then \
echo '*****************************************************************';\
echo 'old coq version detected, double check the diff before committing';\
echo '*****************************************************************';\
Expand Down
2 changes: 1 addition & 1 deletion default.nix
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -4,7 +4,7 @@
bundle ? null, job ? null, inNixShell ? null, src ? ./.,
}@args:
let auto = fetchGit {
url = "https://github.com/coq-community/coq-nix-toolbox.git";
url = "https://github.com/rocq-community/coq-nix-toolbox.git";
ref = "master";
rev = import .nix/coq-nix-toolbox.nix;
};
Expand Down
3 changes: 1 addition & 2 deletions rocq-hierarchy-builder.opam
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,8 +13,7 @@ build: [ [ make "build"]
]
install: [ make "install" ]
depends: [
("coq" {>= "8.18" & < "8.20~"} & "coq-elpi" {>= "2.0"}
| "coq" {>= "8.20" & < "8.21~"} & "coq-elpi" {>= "2.4" | = "dev"}
("coq" {>= "8.20" & < "8.21~"} & "coq-elpi" {>= "2.4" | = "dev"}
| "rocq-core" {(>= "9.0" & < "9.1~") | = "dev"} & "rocq-elpi" {>= "2.4" | = "dev"})
]
conflicts: [
Expand Down
Loading