Update for Coq v8.19, drop support of v8.15 and earlier #47
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Columbus240
force-pushed
the
Fix_for_8.19
branch
from
0e4658c
to
9222d6d
Compare
|
The current failure of the CI with v8.19 is due to rate limiting of the CI. The failures with <= v8.15 are due to the definitions of Even/Odd. |
Columbus240
changed the title
Columbus240
force-pushed
the
Fix_for_8.19
branch
from
8e96700
to
9e45c9b
Compare
The changes in the stdlib regarding `Nat` broke some proofs.
Coq v8.19 dropped the old & deprecated stdlib sections concerning `Even` and `Odd`. The new definitions that need to be used are only available since Coq v8.16. So support for these needs to be dropped or the relevant sections would need to be backported to Coq v8.12 to v8.15. Coq v8.16 was released in September 2022 and according to https://repology.org/project/coq/versions most major distributions have at least v8.16 available. Problem: Hydra-battles uses zorns-lemma as a dependency and currently supports from v8.14 onwards. A new release of zorns-lemma would force hydra-battles to upgrade as well. The problematic parts of the stdlib are only used in `coq-topology` but not in `coq-zorns-lemma`. So it would be possible to only drop support for versions < v8.16 in `coq-topology` and keep the other versions in `coq-zorns-lemma`. But this would require changes in the GitHub-Workflows which I don't yet know how to do.
Concerning real numbers.
Columbus240
force-pushed
the
Fix_for_8.19
branch
from
9e45c9b
to
35979f4
Compare
|
I pushed such changes directly to |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Coq v8.19 dropped the old & deprecated stdlib sections concerning
Evenand
Odd. The new definitions that need to be used are only availablesince Coq v8.16. So support for these needs to be dropped or the
relevant sections would need to be backported to Coq v8.12 to v8.15.
Coq v8.16 was released in September 2022 and according to
https://repology.org/project/coq/versions most major distributions have
at least v8.16 available.
Problem: Hydra-battles uses zorns-lemma as a dependency and currently
supports from v8.14 onwards. A new release of zorns-lemma would force
hydra-battles to upgrade as well.
The problematic parts of the stdlib are only used in
coq-topologybut notin
coq-zorns-lemma. So it would be possible to only drop support forversions < v8.16 in
coq-topologyand keep the other versions incoq-zorns-lemma. But this would require changes in theGitHub-Workflows which I don't yet know how to do.