[coq] Remove Coq build languages 0.1 to 0.7#6445
Closed
ejgallego wants to merge 2 commits intoocaml:mainfrom
Closed
[coq] Remove Coq build languages 0.1 to 0.7#6445ejgallego wants to merge 2 commits intoocaml:mainfrom
ejgallego wants to merge 2 commits intoocaml:mainfrom
Conversation
0d5a086 to
08c6f56
Compare
rgrinberg
reviewed
Nov 11, 2022
src/dune_rules/coq_stanza.ml
Outdated
| Dune_lang.Syntax.create ~name:"coq" ~desc:"the Coq language" | ||
| [ ((0, 1), `Since (1, 9)) | ||
| ; ((0, 2), `Since (2, 5)) | ||
| ; ((0, 3), `Since (2, 8)) |
Member
There was a problem hiding this comment.
That doesn't seem like a good way of deleting old versions. The user will get a confusing message that 0.1 isn't recognized or some such. Instead, we should add a Delete_in constructor here that would give a proper message.
Alizter
reviewed
Nov 12, 2022
9304bc5 to
287ffa0
Compare
As discussed with Ali, we want the previous semantics with implicit global theories to go away ASAP as they don't provide a usable workflow in general. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
Since ocaml#6409 we automatically infer rules for coq-native, and in general this requires at least Coq 8.10 due to the need of command-line option flags added in that version for native. Also, since ocaml#7047 and `(coq lang 0.8)` we detect installed theories, correcting a longstanding problem, we require all users to migrate. The recommended path for most projects is just to upgrade their dune file and Coq version file. Coq 8.10 will likely be the base we support in `(lang coq 1.0)`. Signed-off-by: Emilio Jesus Gallego Arias <e+git@x80.org>
287ffa0 to
0004531
Compare
Collaborator
|
See #8294 for a way to do this. |
Collaborator
Author
|
Superseeded by #12035 |
This was referenced Nov 25, 2025
This file contains hidden or 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
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
4 participants
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.
Since #6409 we automatically infer rules for coq-native, and in general this requires at least Coq 8.10 due to the need of command-line option flags added in that version for native.
The recommended path for most projects is just to upgrade their dune file and Coq version file. Coq 8.10 will likely be the base we support in
(lang coq 1.0).