[new release] coq-lsp (0.1.8+8.17) #24673
Merged
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/saveVo
andcoq/getDocument
requests 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)
fcc
now understands the--coqlib
,--coqcorelib
,--ocamlpath
,-Q
and-R
arguments (@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-lsp
plugin 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)
Goal
andDefinition $id : ... .
as proof starters(@ejgallego, [fleche] [coq] Recognize
Goal
andDefinition $id : ... .
as proof starters ejgallego/coq-lsp#561, reported by @Zimmi48, fixes [fleche] [error rules]Goal
doesn'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-lsp
is 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 )
-rifrom
in_CoqProject
and in command line(
--rifrom
). Thanks to Lasse Blaauwbroek for the report.(@ejgallego, [workspace] Support
-rifrom
option. ejgallego/coq-lsp#581, fixes Support-rifrom
incoq-lsp
arguments 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)
pretac
field 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/selectionRange
request, 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)