[new release] coq-lsp (0.1.7+8.18)

[ejgallego]

Language Server Protocol native server for Coq

• Project page: https://github.com/ejgallego/coq-lsp
• Documentation: https://ejgallego.github.io/coq-lsp/

CHANGES:

---

• New command line compiler fcc. fcc allows to access most
  features 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)
• Enable web extension support. For now this will not try to start
  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)
• Improvements and clenaups on hover display, in particular we don't
  print repeated Notation strings (@ejgallego, [hover] Refactoring and minor fixes. ejgallego/coq-lsp#422)
• Don't fail on missing serlib plugins, they are indeed an
  optimization; this mostly impacts 8.16 by lowering the SerAPI
  requirements (@ejgallego, [loader] Don't fail on missing serlib plugins ejgallego/coq-lsp#421)
• Fix bug that prevented "Goal after tactic" from working properly
  (@ejgallego, [goals] Fix goals_after_tactic option retrieval. ejgallego/coq-lsp#438, reported by David Ilcinkas)
• Fix "Error message browser becomes non-visible when there are many
  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)
• Message about workspace detection was printing the wrong file,
  (@ejgallego, [workspace] Fix message about workspace detection ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern)
• Display the list of pending obligations in info panel (@ejgallego,
  [info panel] Program Obligation support in infoview ejgallego/coq-lsp#262)
• Preliminary support to display document performance data in panel
  (@ejgallego, [code] [protocol] Add notification about document perf data. ejgallego/coq-lsp#181)
• Fix cases when workspace / root URIs are 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 is null. ejgallego/coq-lsp#283)
• Pass implicit argument information to hover printer (@ejgallego, [init] Be more resilient to input, fix bug on workspace parsing ejgallego/coq-lsp#453,
  fixes feature request: Hover should show implicit arguments ejgallego/coq-lsp#448)
• Fix keybinding for the "Show Goals at Point" command (@4ever2, [code] Fix goals command keybind ejgallego/coq-lsp#460)
• Alert when rootPath is relative ([lsp] [init] [workspace] Fix parsing of rootPath ejgallego/coq-lsp#465, @ejgallego, report by Alex
  Sanchez-Stern)
• Hook coq-lsp to ViZX extension (@bhaktishh, Added required support for ViZX Extension ejgallego/coq-lsp#469)
• proof/goals request now takes an optional formatting parameter
  so clients can specify it per-request (@ejgallego, @bhaktishh, [protocol] Include goal output type in goals request ejgallego/coq-lsp#470)
• New command line argument --idle-delay=$secs that controls how
  much an idle server will sleep before going back to request
  processing. Default setting is 0.1, using more aggressive
  settings 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)
• Warnings from _CoqProject files are now applied (@ejgallego,
  reported by @arthuraa, [workspace] Apply warning settings from _CoqProject ejgallego/coq-lsp#500)
• Be more resilient when serializing unknowns Asts (@ejgallego, [getDocument] Be more resilient on unknown ASTs ejgallego/coq-lsp#503,
  reported by Gijs Pennings)
• Coq's STM is not linked anymore to coq-lsp (@ejgallego, [coq] Don't link the STM ejgallego/coq-lsp#511)
• More granular options send_perf_data send_diags, verbosity
  will set them now (@ejgallego, [protocol] Rework verbosity into more granular options. ejgallego/coq-lsp#517)
• Preliminary plugin API for completion events (@ejgallego, [fleche] Add preliminary Document Completion hook ejgallego/coq-lsp#518,
  fixes [controller] Registration for completed API ejgallego/coq-lsp#506)
• Limit the number of messages displayed in the goal window to 101,
  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)

[ejgallego]

This is pending on the merge of #24451 , I'm unsure what the procedure is when doing simultaneous releases.

[mseri]

Usually, after we merge the dependent release, we restart the tests of the PR and review it

[mseri]

The linked PR was closed, so we will wait for the next one (unless I have missed it)

[ejgallego]

Usually, after we merge the dependent release, we restart the tests of the PR and review it

Thanks, I wanted to be sure I was following the right procedure. The new PR is incoming as soon as my own CI passes.

I would be nice if dune-release could prepare simultaneous releases of packages that are not in the same repos, as a single opam repos PR. Would it be OK to implement that kind of workflow?

[ejgallego]

New depending PR #24451

[ejgallego]

Pending PR merged, rebased this PR.

[ejgallego]

CI is now good, sorry for the all the churn, and thanks for all your help folks.

[kit-ty-kate]

Thanks!