[new release] coq-lsp (0.2.0+8.19)

[ejgallego]

Language Server Protocol native server for Coq

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

CHANGES:

---

• [deps] merge serlib into coq-lsp. This allow us to drop the SerAPI
  dependency, and will greatly easy the development of tools that
  require AST manipulation (@ejgallego, [build] [deps] Merge serlib into coq-lsp ejgallego/coq-lsp#698)
• [fleche] Remove 8.16 compatibility layer (@ejgallego, [fleche] Remove FailedPermanent 8.16 hack ejgallego/coq-lsp#747)
• [fleche] Preserve view hint across document changes. With this
  change, we get local continuous checking mode when the view-port
  heuristic is enabled (@ejgallego, [fleche] Preserve view hint across document changes. ejgallego/coq-lsp#748)
• [memo] More precise hashing for Coq states, this improves cache
  performance quite a bit (@ejgallego, [coq] [memo] Better parameters for polymorphic state hashing ejgallego/coq-lsp#751)
• [fleche] Enable sharing of .vo file parsing. This enables better
  sharing, achieving an almost 50% memory reduction for example when
  opening all of HoTT .v files (@ejgallego, @SkySkimmer, @bhaktishh,
  [fleche] Caching / sharing of .vo contents ejgallego/coq-lsp#744)
• [memo] Provide API to query Hashtbl stats (@ejgallego, [memo] Provide Hashtbl stats API ejgallego/coq-lsp#753)
• [nix] Add pet-server deps to flake.nix (Léo Stefanesco, Fix help printing ejgallego/coq-lsp#754)
• [coq-lsp] Fix crash on --help option (Léo Stefanesco, @ejgallego,
  Fix help printing ejgallego/coq-lsp#754)
• [vscode] Fix focus race when a Coq file is in column 2 (@ejgallego,
  [code] Fix focus race when a Coq file is in column 2 ejgallego/coq-lsp#755, cc: Give focus back to Goals panel when navigating proofs ejgallego/coq-lsp#722, [code] Preserve original focus when refocusing the panel. ejgallego/coq-lsp#725)
• [hover] Show input howto for unicode characters on hover
  (@ejgallego, Léo Stefanesco, [hover] Show input help for Unicode characters ejgallego/coq-lsp#756)
• [lsp] [definition] Support for jump to definition across workspace
  files. The location information is obtained from .glob files, so
  it is often not perfect. (@ejgallego, [lsp] Jump to definition for non-local definitions ejgallego/coq-lsp#762, fixes Workspace-wide jump to definition ejgallego/coq-lsp#317)
• [lsp] [hover] Show full name and provenance of identifiers
  (@ejgallego, [lsp] Jump to definition for non-local definitions ejgallego/coq-lsp#762)
• [lsp] [definition] Try also to resolve and locate module imports
  (@ejgallego, [definition] Try to also recognize module names. ejgallego/coq-lsp#764)
• [code] Don't start server on extension activation, unless an editor
  we own is active. We also auto-start the server if a document that
  we own is opened later (@ejgallego, [code] Don't start the language client unless there is an active editor for us ejgallego/coq-lsp#758, fixes coq-lsp connection errors showing in non-Coq projects ejgallego/coq-lsp#750)
• [petanque] Allow init to be called multiple times (@ejgallego,
  @gbdrt, [petanque] Allow init to be called multiple times ejgallego/coq-lsp#766)
• [petanque] Faster query for goals status after run_tac
  (@ejgallego, [petanque] Use lighter goal query on run_tac ejgallego/coq-lsp#768)
• [petanque] New parameter pre_commands to start which allows
  instrumenting the goal before starting the proof (@ejgallego, Alex
  Sanchez-Stern [petanque] Allow to instrument with extra commands before proof start ejgallego/coq-lsp#769)
• [petanque] New http_headers={yes,no} parameter for pet json
  shell, plus some improvements on protocol handling (@ejgallego,
  [petanque] Improvements on protocol handling ejgallego/coq-lsp#770)
• [petanque] Make agent agnostic of environment, allowing embedding
  inside LSP (@ejgallego, [petanque] Make core protocol independent of Coq env runtime ejgallego/coq-lsp#771)
• [diagnostics] Ensure extra diagnostics info is present in all
  errors, not only on those sentences that did parse successfully
  (@ejgallego, Diego Rivera, [diagnostics] Ensure extra diagnostics info is present in all errors ejgallego/coq-lsp#772)
• [hover] New option show_universes_on_hover that will display
  universe data on hover (@ejgallego, @SkySkimmer, [hover] Display debug statistic for universes ejgallego/coq-lsp#666)
• [hover] New plugin unidiff that will elaborate a summary of
  universe data a file, in particular regarding universes added at
  Qed time (@ejgallego, [plugin] Debug plugin for printing universe deltas in files. ejgallego/coq-lsp#773)
• [fleche] Support meta-command Abort All (@ejgallego, [fleche] Support Abort All. ejgallego/coq-lsp#774, fixes
  [vernac] [upstream] Abort All is not supported ejgallego/coq-lsp#550)
• [petanque] Allow memoization control on petanque/run via a new
  parameter memo (@ejgallego, [petanque] Allow memoization control on petanque/run ejgallego/coq-lsp#780)
• [lsp] [petanque] Allow acces to petanque protocol from the lsp
  server (@ejgallego, [lsp] [petanque] Allow access to petanque protocol from the lsp server ejgallego/coq-lsp#778)
• [petanque] Always initialize a workspace. This made pet crash if
  --root was not used and client didn't issue the optimal
  setWorkspace call ([petanque] Always initialize default workspace. ejgallego/coq-lsp#782, @ejgallego, @gbdrt)
• [lsp] [petanque] New methods state/eq and state/hash; this
  allows clients to implement a client-side hash; equality is
  configurable with different methods; moreover, petanque/run can
  compute some extra data like state hashing without a round-trip
  (@ejgallego @gbdrt, [cleanup] Follow-up for #777 , update a few missing places for new API ejgallego/coq-lsp#779)
• [petanque] New methods to hash proof states; use proof state hash
  by default in petanque agent (@ejgallego, @gbdrt, [petanque] Hash proof states instead of system states ejgallego/coq-lsp#808)
• [petanque] New shell method petanque/toc that returns a document
  outline in LSP-style (@ejgallego, [petanque] Add TOC protocol call. ejgallego/coq-lsp#794)

[ejgallego]

Windows CI failed when building a dependency. [Note: our own Windows CI builds OK]

Rest of CI seems fine.

[ejgallego]

Windows CI failed (on this PR and on #26458 and #26459) due to:

• '.' path triggers an unhandled exception on Windows ocamlfind#64
• [windows] staged_pps passes incorrect path separator to cmd.exe dune#10867

[mseri]

Thanks

[ejgallego]

Thanks to you!!!!