-
Notifications
You must be signed in to change notification settings - Fork 1.1k
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.
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
[new release] coq-lsp (0.1.5+8.16) #23319
Merged
Merged
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
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)
CI is fine, failure was on macos-homebrew-ocaml-4.14-amd64 (experimental) while building |
Thanks |
Thanks to you! |
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.
Language Server Protocol native server for Coq
CHANGES:
[doc] [completion] Improve UTF-8 and position validation ejgallego/coq-lsp#270)
$/coq/fileProgress
notification
[info] Fix messages panel rendering after port to react. ejgallego/coq-lsp#272)
offset
field(@ejgallego, [lsp] Make sure ranges are serialized to LSP types ejgallego/coq-lsp#271)
(@artagnon, infoview/goals: fix off-by-one error in goal numbering ejgallego/coq-lsp#277, report by Hugo Herbelin)
(@ejgallego, [fleche] [markdown] Require Coq markdown snippets to use ```coq ejgallego/coq-lsp#280)
documents, see protocol documentation (@ejgallego, [fleche] Generalize contents type ejgallego/coq-lsp#286, reported
by Alex Sanchez-Stern)
[goals] Display hypothesis with bodies. ejgallego/coq-lsp#296, fixes Local definitions are not displayed ejgallego/coq-lsp#293, report by Ali Caglayan)
coq-lsp
incorrectly required the optionalrootPath
initialization parameter, moreover it ignored
rootUri
if presentwhich goes against the LSP spec (@ejgallego, [lsq_init]
rootPath
is optional,rootUri
has precedence. ejgallego/coq-lsp#295, report by AlexSanchez-Stern)
coq-lsp
will now reject opening multiple files when theunderlying Coq version is buggy (@ejgallego, fixes Reject checking multiple documents when Coq < 8.18 ejgallego/coq-lsp#275, fixes
Syntax error for "assert ... by ... " ejgallego/coq-lsp#281)
(@ejgallego [server] [lsp] Fix bug when parsing client option for unicode completion ejgallego/coq-lsp#301)
user-configurable (by default 150) (@ejgallego, [fleche] Stop checking a document when there are too many errors. ejgallego/coq-lsp#303)
using both Coq and Markdown syntax rules (@4ever2, [code] Improve markdown syntax highglighting ejgallego/coq-lsp#307)
(.wpn) Note that we don't associate to them by default, as to allow
the waterproof extension to take over the files (@ejgallego, [contents] Add preliminary waterproof parser. ejgallego/coq-lsp#306)
solved; note still this can be an issue on some client settings
(@ejgallego, [lsp] Abstract URI type, improve URI validation. ejgallego/coq-lsp#313, fixes [server] URI validation ejgallego/coq-lsp#187)
[messages] Enable display of info and debug messages. ejgallego/coq-lsp#314, fixes Support for Typeclasses Debug ejgallego/coq-lsp#308)
goals stack, and focusing information (@ejgallego, [goals] Adapt jsCoq goal printing code to VS Code / React ejgallego/coq-lsp#290, fixes
[info] Port goals2DOM from jsCoq ejgallego/coq-lsp#288, fixes UI for goal focus stack ejgallego/coq-lsp#304, based on jsCoq code by Shachar Itzhaky)
(@ejgallego, [messages] Print warnings in info panel ejgallego/coq-lsp#315, fixes Display warnings in error browser ejgallego/coq-lsp#195)
(@ejgallego, [messages] Print warnings in info panel ejgallego/coq-lsp#315)
(@ejgallego, #, fixes Display warnings in error browser ejgallego/coq-lsp#195)
documentSymbol
return type for newerDocumentSymbol[]
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,
[info] Improve
documentSymbol
request to return extended info. ejgallego/coq-lsp#174, fixes [documentSymbol] Provide extended information, part 1, meta-data ejgallego/coq-lsp#121, [documentSymbol] Provide extended information, part 2, hierarchical information ejgallego/coq-lsp#122)amend states, required for [doc] [error] Auto-admit bullets on new bullet error. ejgallego/coq-lsp#319 (@ejallego, [fleche] Allow error recovery to execute dynamic commands ejgallego/coq-lsp#320)
opened due to an unsolved previous bullet. This also works for {}
focusing operators. This is very useful when navigating bulleted
proofs (@ejgallego, @Alizter, [doc] [error] Auto-admit bullets on new bullet error. ejgallego/coq-lsp#319, fixes Auto admit goal selectors ejgallego/coq-lsp#300)
metadata, this only works inside the same file (@ejgallego, [lsp] Basic jump to definition support. ejgallego/coq-lsp#318)
Type inference on hover ejgallego/coq-lsp#164)