[coq] Remove Coq build languages 0.1 to 0.7 #6445
Draft
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
ejgallego
force-pushed
the
coq_lang_remove_810
branch
from
0d5a086 to
08c6f56
Compare
rgrinberg
reviewed
Nov 11, 2022
src/dune_rules/coq_stanza.ml
Outdated
| @@ -3,9 +3,7 @@ open Dune_lang.Decoder | |||
|
|
|||
| let coq_syntax = | |||
| 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)) | |||
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
ejgallego
force-pushed
the
coq_lang_remove_810
branch
2 times, most recently
from
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 <[email protected]>
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 <[email protected]>
ejgallego
force-pushed
the
coq_lang_remove_810
branch
from
287ffa0 to
0004531
Compare
ejgallego
changed the title
|
See #8294 for a way to do this. |
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.
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).