[new release] coq-lsp (0.2.4+9.1)

[ejgallego]

Language Server Protocol native server for Coq

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

CHANGES:

---

• [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
  remove our own local wrapper (@ejgallego, [goaldump] Also serialize goals in sexp format. ejgallego/coq-lsp#975).
• [petanque] New petanque/ast and petanque/ast_at_pos
  (@ejgallego, @JulesViennotFranca, [petanque] Add new methods to get ast from string and from document. ejgallego/coq-lsp#980)
• [serlib] Support for generic Ast analyzers. This opens the door to
  many feature requests such as syntax coloring, dependency
  extraction, etc... (@ejgallego, @JulesViennotFranca, [serlib] Support for generic Ast analyzers ejgallego/coq-lsp#981)
• [fleche] Support "rocq" markdown delimiters in .mv files
  (@ejgallego, [fleche] Support "rocq" markdown delimiters in .mv files ejgallego/coq-lsp#987)
• [workspace] Support _RocqProject (@ejgallego, [fleche] Support _RocqProject ejgallego/coq-lsp#988, fixes [workspace] Support _RocqProject ejgallego/coq-lsp#934)
• [lsp] [getDocument] Allow to get goals in one shot. We also
  refactor the response type to accommodate different
  meta-data. Note: (!) breaking change. (@ejgallego, [lsp] [getDocument] Allow to get goals in one shot. ejgallego/coq-lsp#985, fixes
  Missing of_yojson for FlecheDocument module ejgallego/coq-lsp#862, thanks to the Alectryon team)
• [lsp] Better error handling in URI parsing (@ejgallego, [lsp] Don't raise on URI parsing error. ejgallego/coq-lsp#994, thanks to
  Adrien from Zulip)
• [lsp] Better protocol-level handling for our non-standard Lang.Point
  and Lang.Diagnostic types, via global flags that allow us to
  choose the input/output representation for non-standard field such
  as [Point.offset]. This ensures that leaks of these non-standard
  fields are rarer. (@ejgallego, [lsp] Handle protocol extensions better ejgallego/coq-lsp#995, cc LSP improvements tracker issue ejgallego/coq-lsp#279, cc [build] Common LSP libraries ejgallego/coq-lsp#2, thanks to
  Adrien from Zulip)
• [lsp] [completion] Rework completion configuration into a
  coq-lsp.completion json object. The unicode_completion setting
  is now deprecated, and has been replaced by
  completion.unicode.enable (@ejgallego, Configurable completion chars ejgallego/coq-lsp#993)
• [lsp] [completion] [vscode] Unicode completion commit characters
  are now configurable via the server setting variable
  completion.unicode.commit_chars. (@Durbatuluk1701, Configurable completion chars ejgallego/coq-lsp#993)
• [goals] [config] New (global) option for goal display method
  proof/goals: messages_follow_goal. If true, proof/goals
  will show errors and messages for the same sentence goals are
  shown; if false, it will always show errors and messages for the
  specified position, if there is a Rocq sentence at hand
  (@jpoiret, @ejgallego, [lsp] Return executed sentence info in goal request. ejgallego/coq-lsp#999, fixes: error field of proof/goals does not respect goal_after_tactic ejgallego/coq-lsp#941)
• [coq] Install full state before parsing. Before we did only
  Pcoq.unfreeze but that is not enough, in particular the call to
  get_default_proof_mode will not be correct (@ejgallego, @pimotte,
  [coq] [bugfix] Set state properly before parsing ejgallego/coq-lsp#1011, fixes [bug] Properly handle proof mode ejgallego/coq-lsp#656)
• [misc] Don't depend on Jane Street's base (@patrick-nicodemus
  @ejgallego, Base is not present in opam dependencies ejgallego/coq-lsp#1004)
• [wasm worker] Add WebAssembly based worker based on waCoq. This is
  now the default for the .vsix binary build. For now, we include
  Rocq's Stdlib and Waterproof (@corwin-of-amber, @ejgallego,
  @pimotte, [web worker] WASM-based Web Worker ejgallego/coq-lsp#1008, cc JS Worker Meta Issue ejgallego/coq-lsp#833, fixes [js worker] Scheduling and interruption problems ejgallego/coq-lsp#907, fixes [js] WebAssembly Support ejgallego/coq-lsp#908, fixes [web] Web extension download the Coq filesystem uncompressed. ejgallego/coq-lsp#913)
• [opam] Added x-maintenance-intent intent field. (@ejgallego,
  [opam] Added x-maintenance-intent field. ejgallego/coq-lsp#1020)
• [lsp] [didOpen] languageId now takes priority over uri extension
  in LSP didOpen. (@ejgallego, [lsp] [didOpen] Respect languageId parameter ejgallego/coq-lsp#1021, fixes Processing Coq sources extracted from .rst/.md files ejgallego/coq-lsp#1005)
• [coq] incorporate experimental coq-layout-engine printer, both in
  client and server parts (@ejgallego, [layout engine] Move Coq Layout engine tree to coq-lsp repos. ejgallego/coq-lsp#668, see also [roadmap] coq-layout-engine general issue ejgallego/coq-lsp#72 and
  [draft] New printer prototype jscoq/jscoq#282 )
• [lsp] [code] New notification $/coq/executionInformation which
  will signal clients when rocq-lsp does intent to start to execute a
  sentence. Experimentally, this is used to provide a red glow on
  long-running commands in coq-lsp/VSCode, to provide better user
  feedback on long-running commands (@ejgallego, suggested by
  @jpoiret, [lsp] [fleche] New notification $/coq/executionInformation ejgallego/coq-lsp#1002)
• [lsp] [outline] Support Notation, Ltac and Ltac Notation in
  outline entries (@ejgallego, [coq] [serlib] Ast analysis / outline for Notation, Ltac, and Tactic Notation ejgallego/coq-lsp#1025, fixes Ltac, Notation and Tactic Notation doesn't appear in the document overview ejgallego/coq-lsp#632)

[jmid]

AFAICS, this requires a rocq-core version not yet released to the opam-repo, thus causing Failed - Everything was skipped and coq-lsp.0.2.4+9.1 (failed: [SKIP] Package not available) on all workflows.

[ejgallego]

Indeed, it seems Rocq 9.1 didn't reach the opam archive yet. I'll rebase and ping once that happens.