[new release] coq-lsp (0.1.8+8.18) #24672
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: ------------------------------- - Update VSCode client dependencies, should bring some performance improvements to goal pretty printing (@ejgallego, ejgallego/coq-lsp#530) - Update goal display colors for light mode so they are actually readable now. (@bhaktishh, ejgallego/coq-lsp#539, fixes ejgallego/coq-lsp#532) - Added link to Python coq-lsp client by Pedro Carrot and Nuno Saavedra (@Nfsaavedra, ejgallego/coq-lsp#536) - Properly concatenate warnings from _CoqProject (@ejgallego, reported by @mituharu, ejgallego/coq-lsp#541, fixes ejgallego/coq-lsp#540) - Fix broken `coq/saveVo` and `coq/getDocument` requests due to a parsing problem with extra fields in their requests (@ejgallego, ejgallego/coq-lsp#547, reported by @Zimmi48) - `fcc` now understands the `--coqlib`, `--coqcorelib`, `--ocamlpath`, `-Q` and `-R` arguments (@ejgallego, ejgallego/coq-lsp#555) - Describe findlib status in `Workspace.describe`, which is printed in the output windows (@ejgallego, ejgallego/coq-lsp#556) - `coq-lsp` plugin loader will now be strict in case of a plugin failure, the previous loose behavior was more convenient for the early releases, but it doesn't make sense now and made things pretty hard to debug on the Windows installer (@ejgallego, ejgallego/coq-lsp#557) - Add pointers to Windows installers (@ejgallego, ejgallego/coq-lsp#559) - Recognize `Goal` and `Definition $id : ... .` as proof starters (@ejgallego, ejgallego/coq-lsp#561, reported by @Zimmi48, fixes ejgallego/coq-lsp#548) - Provide basic notation information on hover. This is intended for people to build their own more refined notation feedback systems (@ejgallego, ejgallego/coq-lsp#562) - Hover request can now be extended by plugins (@ejgallego, ejgallego/coq-lsp#562) - Updated LSP and JS client libs, notably to vscode-languageclient 9 (@ejgallego, ejgallego/coq-lsp#565) - Implement a LIFO document scheduler, this is heavier in the background as more documents will be checked, but provides a few usability improvements (@ejgallego, ejgallego/coq-lsp#566, fixes ejgallego/coq-lsp#563, reported by Ali Caglayan) - New lexical qed detection error recovery rule; this makes a very large usability difference in practice when editing inside proofs. (@ejgallego, ejgallego/coq-lsp#567, fixes ejgallego/coq-lsp#33) - `coq-lsp` is now supported by the `coq-nix-toolbox` (@Zimmi48, @CohenCyril, ejgallego/coq-lsp#572, via coq-community/coq-nix-toolbox#164 ) - Support for `-rifrom` in `_CoqProject` and in command line (`--rifrom`). Thanks to Lasse Blaauwbroek for the report. (@ejgallego, ejgallego/coq-lsp#581, fixes ejgallego/coq-lsp#579) - Export Query Goals API in VSCode client; this way other extensions can implement their own commands that query Coq goals (@amblafont, @ejgallego, ejgallego/coq-lsp#576, closes ejgallego/coq-lsp#558) - New `pretac` field for preprocessing of goals with a tactic using speculative execution, this is experimental for now (@amblafont, @ejgallego, ejgallego/coq-lsp#573, helps with ejgallego/coq-lsp#558) - Implement `textDocument/selectionRange` request, that will return the range of the Coq sentence underlying the cursor. In VSCode, this is triggered by the "Expand Selection" command. The implementation is partial: we only take into account the first position, and we only return a single range (Coq sentence) without parents. (@ejgallego, ejgallego/coq-lsp#582) - Be more robust to mixed-separator windows paths in workspace detection (@ejgallego, ejgallego/coq-lsp#583, fixes ejgallego/coq-lsp#569) - Adjust printing breaks in error and message panels (@ejgallego, @Alizter, ejgallego/coq-lsp#586, fixes ejgallego/coq-lsp#457 , fixes ejgallego/coq-lsp#458 , fixes ejgallego/coq-lsp#571)
|
CI failure is which seems unrelated to me. |
|
Thanks! You may want to announce this on https://discuss.ocaml.org, where we have a Community category and an |
|
Thanks!! |
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:
improvements to goal pretty printing (@ejgallego, [client] Update package.json dependencies ejgallego/coq-lsp#530)
readable now. (@bhaktishh, Color changes for light color themes. ejgallego/coq-lsp#539, fixes Fixed light color in the goal panel ejgallego/coq-lsp#532)
Saavedra (@Nfsaavedra, [doc] Add Python client to README ejgallego/coq-lsp#536)
reported by @mituharu, [coq] Properly concatenate warnings ejgallego/coq-lsp#541, fixes Multiple warning display options in _CoqProject are not handled correctly ejgallego/coq-lsp#540)
coq/saveVoandcoq/getDocumentrequests due to aparsing problem with extra fields in their requests (@ejgallego,
[lsp] Fix bug when retrieving URIs from document params ejgallego/coq-lsp#547, reported by @Zimmi48)
fccnow understands the--coqlib,--coqcorelib,--ocamlpath,-Qand-Rarguments (@ejgallego, [fcc] Understand arguments for Coq environment ejgallego/coq-lsp#555)Workspace.describe, which is printedin the output windows (@ejgallego, [coq] Output findlib workspace status in workspace describe. ejgallego/coq-lsp#556)
coq-lspplugin loader will now be strict in case of a pluginfailure, the previous loose behavior was more convenient for the
early releases, but it doesn't make sense now and made things
pretty hard to debug on the Windows installer (@ejgallego, [coq] [loader] Don't swallow plugin loading errors. ejgallego/coq-lsp#557)
GoalandDefinition $id : ... .as proof starters(@ejgallego, [fleche] [coq] Recognize
GoalandDefinition $id : ... .as proof starters ejgallego/coq-lsp#561, reported by @Zimmi48, fixes [fleche] [error rules]Goaldoesn't trigger error recovery mode for theorems. ejgallego/coq-lsp#548)people to build their own more refined notation feedback systems
(@ejgallego, [hover] Refactor providers into plugins, add basic notation display. ejgallego/coq-lsp#562)
(@ejgallego, [client] Update vscode client and misc js packages ejgallego/coq-lsp#565)
background as more documents will be checked, but provides a few
usability improvements (@ejgallego, [fleche] Implement document scheduler ejgallego/coq-lsp#566, fixes edit needed to start client after a restart ejgallego/coq-lsp#563, reported by
Ali Caglayan)
large usability difference in practice when editing inside proofs.
(@ejgallego, [fleche] [error] Detect Qed based on buffer contents ejgallego/coq-lsp#567, fixes Better parsing error recovery for bad parsing inside a proof. ejgallego/coq-lsp#33)
coq-lspis now supported by thecoq-nix-toolbox(@Zimmi48,@CohenCyril, Add mention of the Coq Nix Toolbox. ejgallego/coq-lsp#572, via
Add coq-lsp server in nix-shell when available. coq-community/coq-nix-toolbox#164 )
-rifromin_CoqProjectand in command line(
--rifrom). Thanks to Lasse Blaauwbroek for the report.(@ejgallego, [workspace] Support
-rifromoption. ejgallego/coq-lsp#581, fixes Support-rifromincoq-lsparguments ejgallego/coq-lsp#579)can implement their own commands that query Coq goals (@amblafont,
@ejgallego, [client] [vscode] Export Query Goals API ejgallego/coq-lsp#576, closes [vscode client] graph-editor integration ejgallego/coq-lsp#558)
pretacfield for preprocessing of goals with a tactic usingspeculative execution, this is experimental for now (@amblafont,
@ejgallego, [README] [nix] Add changes + tweak on the README. ejgallego/coq-lsp#573, helps with [vscode client] graph-editor integration ejgallego/coq-lsp#558)
textDocument/selectionRangerequest, that will returnthe range of the Coq sentence underlying the cursor. In VSCode,
this is triggered by the "Expand Selection" command. The
implementation is partial: we only take into account the first
position, and we only return a single range (Coq sentence) without
parents. (@ejgallego, [lsp] Implement
textDocument/selectionRange. ejgallego/coq-lsp#582)detection (@ejgallego, [workspace] [windows] Tolerate better Windows paths with mixed path separators ejgallego/coq-lsp#583, fixes [windows] Workspace reverse lookup code is not robust to windows paths ejgallego/coq-lsp#569)
@Alizter, [info view] Adjust breaks in errors and messages panels. ejgallego/coq-lsp#586, fixes Printing records has no new lines ejgallego/coq-lsp#457 , fixes Printing a module has no new lines or component disambiguation ejgallego/coq-lsp#458 , fixes Formatting of terms missing in error messages ejgallego/coq-lsp#571)