Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Reject checking multiple documents when Coq < 8.18 #275

Closed
ejgallego opened this issue Feb 2, 2023 · 1 comment · Fixed by #287 or ocaml/opam-repository#23319
Closed

Reject checking multiple documents when Coq < 8.18 #275

ejgallego opened this issue Feb 2, 2023 · 1 comment · Fixed by #287 or ocaml/opam-repository#23319
Labels
kind: bug Something isn't working kind: internal kind: upstream part: lsp server
Milestone
0.1.5

Comments

@ejgallego
Copy link
Owner

This is indeed very frustating for users, so indeed let's just do this for 8.18, and produce an error message for 8.17 and 8.16.
@ejgallego ejgallego added this to the 0.1.5 milestone Feb 2, 2023
@ejgallego
Copy link
Owner Author

Instead I have backported the fix to 8.17, so we could have users workaround this issue more easily.

ejgallego added a commit that referenced this issue Feb 6, 2023
@ejgallego
[fleche] Reject opening multiple Coq documents for buggy Coq versions.
dc0afa0 
Fixes #275

We use a heuristic in the fixed up branches as follows: if the Coq
version contains LSP, then we assume the fix has been backported.

That should work when doing `opam pin`.
ejgallego added a commit that referenced this issue Feb 6, 2023
@ejgallego
[fleche] Reject opening multiple Coq documents for buggy Coq versions.
297c42d 
Fixes #275

We use a heuristic in the fixed up branches as follows: if the Coq
version contains LSP, then we assume the fix has been backported.

That should work when doing `opam pin`.
@ejgallego ejgallego mentioned this issue Feb 6, 2023
Merged
ejgallego added a commit that referenced this issue Feb 6, 2023
@ejgallego
[fleche] Reject opening multiple Coq documents for buggy Coq versions.
041ff7b 
Fixes #275

We use a heuristic in the fixed up branches as follows: if the Coq
version contains LSP, then we assume the fix has been backported.

That should work when doing `opam pin`.
ejgallego added a commit that referenced this issue Feb 6, 2023
@ejgallego
[fleche] Reject opening multiple Coq documents for buggy Coq versions.
c26a6cf 
Fixes #275

We use a heuristic in the fixed up branches as follows: if the Coq
version contains LSP, then we assume the fix has been backported.

That should work when doing `opam pin`.
ejgallego added a commit that referenced this issue Feb 6, 2023
@ejgallego
[fleche] Reject opening multiple Coq documents for buggy Coq versions.
3f36a86 
Fixes #275

We use a heuristic in the fixed up branches as follows: if the Coq
version contains LSP, then we assume the fix has been backported.

That should work when doing `opam pin`.
ejgallego added a commit that referenced this issue Feb 7, 2023
@ejgallego
[fleche] Reject opening multiple Coq documents for buggy Coq versions.
6dd0231 
Fixes #275 , #281

We use a heuristic in the fixed up branches as follows: if the Coq
version contains LSP, then we assume the fix has been backported.

That should work when doing `opam pin`.
@ejgallego ejgallego mentioned this issue Feb 15, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Feb 15, 2023
@ejgallego
[new release] coq-lsp (0.1.5+8.16)
b7a2330 
CHANGES:

---------------------

 - Fix a bug when trying to complete in an empty file (@ejgallego,
   ejgallego/coq-lsp#270)
 - Fix a bug with the position reported by the `$/coq/fileProgress`
   notification
 - Fix messages panel rendering after the port to React (@ejgallego,
   ejgallego/coq-lsp#272)
 - Fix non-compliance with LSP range type due to extra `offset` field
   (@ejgallego, ejgallego/coq-lsp#271)
 - The goal display now numbers goals starting with 1 instead of 0
   (@artagnon, ejgallego/coq-lsp#277, report by Hugo Herbelin)
 - Markdown Coq code blocks now must specify "coq" as a language
   (@ejgallego, ejgallego/coq-lsp#280)
 - Server is now more strict w.r.t. what URIs it will accept for
   documents, see protocol documentation (@ejgallego, ejgallego/coq-lsp#286, reported
   by Alex Sanchez-Stern)
 - Hypotheses with bodies are now correctly displayed (@ejgallego,
   ejgallego/coq-lsp#296, fixes ejgallego/coq-lsp#293, report by Ali Caglayan)
 - `coq-lsp` incorrectly required the optional `rootPath`
   initialization parameter, moreover it ignored `rootUri` if present
   which goes against the LSP spec (@ejgallego, ejgallego/coq-lsp#295, report by Alex
   Sanchez-Stern)
 - `coq-lsp` will now reject opening multiple files when the
   underlying Coq version is buggy (@ejgallego, fixes ejgallego/coq-lsp#275, fixes
   ejgallego/coq-lsp#281)
 - Fix bug when parsing client option for unicode completion
   (@ejgallego ejgallego/coq-lsp#301)
 - Support unicode characters in filenames (@artagnon, ejgallego/coq-lsp#302)
 - Stop checking documents after a maximum number of errors,
   user-configurable (by default 150) (@ejgallego, ejgallego/coq-lsp#303)
 - Coq Markdown files (.mv extension) are now highlighted properly
   using both Coq and Markdown syntax rules (@4ever2, ejgallego/coq-lsp#307)
 - Goal view now supports find (@Alizter, ejgallego/coq-lsp#309, closes ejgallego/coq-lsp#305)
 - coq-lsp now understands a basic version of Coq Waterproof files
   (.wpn) Note that we don't associate to them by default, as to allow
   the waterproof extension to take over the files (@ejgallego, ejgallego/coq-lsp#306)
 - URI validation is now more strict, and some further bugs should be
   solved; note still this can be an issue on some client settings
   (@ejgallego, ejgallego/coq-lsp#313, fixes ejgallego/coq-lsp#187)
 - Display Coq info and debug messages in info panel (@ejgallego,
   ejgallego/coq-lsp#314, fixes ejgallego/coq-lsp#308)
 - Goal display handles background goals better, showing preview,
   goals stack, and focusing information (@ejgallego, ejgallego/coq-lsp#290, fixes
   ejgallego/coq-lsp#288, fixes ejgallego/coq-lsp#304, based on jsCoq code by Shachar Itzhaky)
 - Warnings are now printed in the info view messages panel
   (@ejgallego, ejgallego/coq-lsp#315, fixes ejgallego/coq-lsp#195)
 - Info protocol messages now have location and level
   (@ejgallego, ejgallego/coq-lsp#315)
 - Warnings are not printed in the info view messages panel
   (@ejgallego, #, fixes ejgallego/coq-lsp#195)
 - Improved `documentSymbol` return type for newer `DocumentSymbol[]`
   hierarchical symbol support. This means that sections and modules
   will now be properly represented, as well as constructors for
   inductive types, projections for records, etc...  (@ejgallego,
   ejgallego/coq-lsp#174, fixes ejgallego/coq-lsp#121, ejgallego/coq-lsp#122)
 - [internal] Error recovery can now execute full Coq commands as to
   amend states, required for ejgallego/coq-lsp#319 (@ejallego, ejgallego/coq-lsp#320)
 - Auto-admit the previous bullet goal when a new bullet cannot be
   opened due to an unsolved previous bullet. This also works for {}
   focusing operators. This is very useful when navigating bulleted
   proofs (@ejgallego, @Alizter, ejgallego/coq-lsp#319, fixes ejgallego/coq-lsp#300)
 - Store Ast.Info.t incrementally (@ejgallego, ejgallego/coq-lsp#337, fixes ejgallego/coq-lsp#316)
 - Basic jump to definition support; due to lack of workspace
   metadata, this only works inside the same file (@ejgallego, ejgallego/coq-lsp#318)
 - Show type of identifiers at point on hover (@ejgallego, ejgallego/coq-lsp#321, cc:
   ejgallego/coq-lsp#164)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
kind: bug Something isn't working kind: internal kind: upstream part: lsp server
Projects
None yet
Milestone
0.1.5
1 participant
@ejgallego