[ANN] coq-lsp 0.2.4

Announcements
, ,
1

Dear all,

We’re happy to announce the 0.2.4 release of coq-lsp.

This release contains some bug fixes and refinements, and a few
important new features:

  • the extension includes a Rocq 9.1 WebAssembly version that can be
    used directly without installation, using Shachar Itzhaky’s
    excellent ocaml-wasm jsCoq port.

    To use Rocq online, go to vscode.dev or github.dev and install
    the coq-lsp VSCode extension. That should be it!

    As of now, only Rocq’s Stdlib is available. See the coq-lsp FAQ
    for more information.

  • Official Alectryon support.

  • Support for Rocq 9.1, _RocqProject, rocq markdown and LaTeX
    codeblocks.

  • Support for Notation, Ltac, and Ltac Notation in document
    outlines.

  • A new visual feedback mode that will highlight Rocq sentences that
    take a long time to process by making them glow in VSCode.

  • The experimental “layout printer” has been merged.

  • Better configuration for completion.

We’d like to thank all the contributors, testers, and bug reporters
for their work on the 0.2.4 release.

Detailed changelog:

coq-lsp 0.2.4: (W)Activation

  • [js] [deps] Bump to findlib 1.9.8, use vanilla API for loading and
    remove our own local wrapper (@ejgallego, #975).
  • [petanque] New petanque/ast and petanque/ast_at_pos (@ejgallego@JulesViennotFranca, #980)
  • [serlib] Support for generic Ast analyzers. This opens the door to
    many feature requests such as syntax coloring, dependency
    extraction, etc… (@ejgallego, @JulesViennotFranca, #981)
  • [fleche] Support “rocq” markdown delimiters in .mv files
    (@ejgallego, #987)
  • [workspace] Support _RocqProject (@ejgallego, #988, fixes #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, #985, fixes
    #862, thanks to the Alectryon team)
  • [lsp] Better error handling in URI parsing (@ejgallego, #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, #995, cc #279, cc #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, #993)
  • [lsp] [completion] [vscode] Unicode completion commit characters
    are now configurable via the server setting variable
    completion.unicode.commit_chars. (@Durbatuluk1701, #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, #999, fixes: #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,
    #1011, fixes #656)
  • [misc] Don’t depend on Jane Street’s base (@patrick-nicodemus
    @ejgallego, #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, #1008, cc #833, fixes #907, fixes #908, fixes #913)
  • [opam] Added x-maintenance-intent intent field. (@ejgallego,
    #1020)
  • [lsp] [didOpen] languageId now takes priority over uri extension
    in LSP didOpen. (@ejgallego, #1021, fixes #1005)
  • [coq] incorporate experimental coq-layout-engine printer, both in
    client and server parts (@ejgallego, #668, see also #72 and
    [draft] New printer prototype by ejgallego · Pull Request #282 · jscoq/jscoq · GitHub )
  • [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 (@ejgallego, suggested by @jpoiret, #1002)
1 Like