Skip to content

Commit

Permalink
Do not support coq < v8.16 anymore
Browse files Browse the repository at this point in the history
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.
  • Loading branch information
Columbus240 committed Aug 6, 2024
1 parent 9222d6d commit 8e96700
Show file tree
Hide file tree
Showing 4 changed files with 3 additions and 7 deletions.
4 changes: 0 additions & 4 deletions .github/workflows/coq-ci.yml
Original file line number Diff line number Diff line change
Expand Up @@ -20,10 +20,6 @@ jobs:
- 'coqorg/coq:8.18'
- 'coqorg/coq:8.17'
- 'coqorg/coq:8.16'
- 'coqorg/coq:8.15'
- 'coqorg/coq:8.14'
- 'coqorg/coq:8.13'
- 'coqorg/coq:8.12'
fail-fast: false
steps:
- uses: actions/checkout@v2
Expand Down
2 changes: 1 addition & 1 deletion README.md
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,7 @@ and results of general topology in Coq.
- stop-cran ([**@stop-cran**](https://github.com/stop-cran))
- Columbus240 ([**@Columbus240**](https://github.com/Columbus240))
- License: [GNU Lesser General Public License v2.1 or later](LICENSE)
- Compatible Coq versions: Coq 8.12 or later (use the corresponding branch or release for other Coq versions)
- Compatible Coq versions: Coq 8.16 or later (use the corresponding branch or release for other Coq versions)
- Additional dependencies:
- Zorn's Lemma (set library that is part of this repository)
- Coq namespace: `Topology`
Expand Down
2 changes: 1 addition & 1 deletion coq-topology.opam
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ and results of general topology in Coq.
build: ["dune" "build" "-p" name "-j" jobs]
depends: [
"dune" {>= "2.5"}
"coq" {(>= "8.12" & < "8.20~") | (= "dev")}
"coq" {(>= "8.16" & < "8.20~") | (= "dev")}
"coq-zorns-lemma" {= version}
]

Expand Down
2 changes: 1 addition & 1 deletion coq-zorns-lemma.opam
Original file line number Diff line number Diff line change
Expand Up @@ -17,7 +17,7 @@ was as support for the Topology library.
build: ["dune" "build" "-p" name "-j" jobs]
depends: [
"dune" {>= "2.5"}
"coq" {(>= "8.12" & < "8.20~") | (= "dev")}
"coq" {(>= "8.16" & < "8.20~") | (= "dev")}
]

tags: [
Expand Down

0 comments on commit 8e96700

Please sign in to comment.