[new release] coq-lsp (0.1.7+8.17) #24080
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:
fcc
.fcc
allows to access mostfeatures of
coq-lsp
without the need for a command line client,and it has been designed to be extensible and machine-friendly
(@ejgallego, [compiler] Flèche-based command line compiler. ejgallego/coq-lsp#507, fixes [meta] Standalone compiler ejgallego/coq-lsp#472)
the coq-lsp worker as it is not yet built. (@ejgallego, [code] Enable web extension support. ejgallego/coq-lsp#430, fixes
[code] Enable web extension ejgallego/coq-lsp#234)
print repeated
Notation
strings (@ejgallego, [hover] Refactoring and minor fixes. ejgallego/coq-lsp#422)optimization; this mostly impacts 8.16 by lowering the SerAPI
requirements (@ejgallego, [loader] Don't fail on missing serlib plugins ejgallego/coq-lsp#421)
(@ejgallego, [goals] Fix goals_after_tactic option retrieval. ejgallego/coq-lsp#438, reported by David Ilcinkas)
goals" by using a fixed-position separated error display (@TDiazT,
Progress indicator and comments don't interact correctly ejgallego/coq-lsp#445, fixes Error message browser becomes non-visible when there are many goals. ejgallego/coq-lsp#441)
(@ejgallego, [workspace] Fix message about workspace detection ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern)
[info panel] Program Obligation support in infoview ejgallego/coq-lsp#262)
(@ejgallego, [code] [protocol] Add notification about document perf data. ejgallego/coq-lsp#181)
null
, as per LSP spec,([init] Be more resilient to input, fix bug on workspace parsing ejgallego/coq-lsp#453 , reported by orilahav, fixes [server] Initialize request doesn't handle properly the case where
workspaceFolders
isnull
. ejgallego/coq-lsp#283)fixes feature request: Hover should show implicit arguments ejgallego/coq-lsp#448)
rootPath
is relative ([lsp] [init] [workspace] Fix parsing of rootPath ejgallego/coq-lsp#465, @ejgallego, report by AlexSanchez-Stern)
proof/goals
request now takes an optional formatting parameterso clients can specify it per-request (@ejgallego, @bhaktishh, [protocol] Include goal output type in goals request ejgallego/coq-lsp#470)
--idle-delay=$secs
that controls howmuch an idle server will sleep before going back to request
processing. Default setting is
0.1
, using more aggressivesettings like
0.01
can decrease latency of requests by ~4x(@ejgallego, @HazardousPeach, Reduce thread delay in process queue for a speedup on short commands ejgallego/coq-lsp#467, [controller] [native] New parameter --idle-delay ejgallego/coq-lsp#471)
_CoqProject
files are now applied (@ejgallego,reported by @arthuraa, [workspace] Apply warning settings from _CoqProject ejgallego/coq-lsp#500)
reported by Gijs Pennings)
coq-lsp
(@ejgallego, [coq] Don't link the STM ejgallego/coq-lsp#511)send_perf_data
send_diags
,verbosity
will set them now (@ejgallego, [protocol] Rework verbosity into more granular options. ejgallego/coq-lsp#517)
fixes [controller] Registration for completed API ejgallego/coq-lsp#506)
as to workaround slow render of Coq's pretty printing format. This
is an issue for example in Search where we can get thousand of
results. We also speed up the rendering a bit by not hashing twice,
and fix a parameter-passing bug. (@ejgallego, [vscode] Limit the number of messages displayed in the goal window ejgallego/coq-lsp#523, reported by
Anton Podkopaev)