search

coq-community / topology

General topology in Coq [maintainers=@amiloradovsky,@Columbus240,@stop-cran]
Other
46 stars 10 forks source link

Update for Coq v8.19, drop support of v8.15 and earlier #47

Closed Columbus240 closed 1 month ago

Columbus240 commented 1 month ago

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.

Columbus240 commented 1 month ago

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 commented 1 month ago

I pushed such changes directly to master.