Coq LSP release 0.1.2

Dear all,

we are happy to announce the release of coq-lsp 0.1.2, a new language Server and VSCode extension for the Coq interactive proof assistant.

coq-lsp aims to provide a modern and streamlined proof-editing experience, supporting incremental checking, markdown documents, and an error recovery strategy friendly to step wise development of proof documents.

The 0.1.2 release has been significantly improved since the 0.1.0 preview release, we encourage Visual Studio Code users to try it!

(make sure that the client and server version coincide, and see below for known issues)

See the coq-lsp F.A.Q. [1] for some often asked questions.

Don’t hesitate to stop by our Zulip [2] channel to chat, provide feedback, or report bugs.

coq-lsp is developed in an open, collaborative way, if you are interested in helping, we are really looking forward to it. There are many interesting projects that can be done with coq-lsp as a base.

The first coq-lsp developers and user online meeting will take place Monday January 9th, at 5pm Paris time, see [3] for details.

The main known issue is that coq-lsp won’t properly handle yet proving with multiple buffers, this is due to problems in Coq upstream, Coq developers and in particular Gaëtan Gilbert are working in a fix.

If you find this issue, simply close all other .v files and restart the server.

The full changelog for this release is:

coq-lsp 0.1.2: Message

  • Send an error to the client if the client and server versions don’t
    match (@ejgallego, #126)
  • Parse options -noinit, -indices-matter, and -impredicative-set from
    _CoqProject (@artagnon, @ejgallego, #140, #150)
  • Log file log-lsp.txt has been removed in favor of coq-lsp.trace.server
    (@artagnon, @ejgallego, #130, #148)
  • Added --bt flag to print a backtrace on error (@Alizter, #147)
  • A detailed view of Coq errors is now displayed in the info panel
    (@ejgallego, #128)
  • Coq “Notice” messages, such as the ones generated by About or
    Search are not shown anymore as diagnostics. Instead, they will
    be shown on the side panel when clicking on the corresponding
    command. The show_notices_as_diagnostics option allows to restore
    old behavior (@ejgallego, #128, fixes #125)
  • Print some more info about Coq workspace configuration (@ejgallego, #151)
  • Admit failed Qed by default; allow users to configure it
    (@ejgallego, #118, fixes #90)

coq-lsp 0.1.1: Location

  • Don’t crash if the log file can’t be created (@ejgallego, #87)
  • Use LSP functions for client-side logging (@ejgallego, #87)
  • Log _CoqProject detection settings to client window (@ejgallego, #88)
  • Use plugin include paths from _CoqProject (@ejgallego, #88)
  • Support OCaml >= 4.12 (@ejgallego, #93)
  • Optimize the number of diagnostics sent in eager mode (@ejgallego, #104)
  • Improved syntax highlighting on VSCode client (@artagnon, #105)
  • Resume document checking from the point it was interrupted
    (@ejgallego, #95, #99)
  • Don’t convert Coq “Info” messages such as “Foo is defined” to
    feedback by default; users willing to see them can set the
    corresponding option (@ejgallego, #113)
  • Send $/coq/fileProgress progress notifications from server,
    similarly to what Lean does; display them in Code’s right gutter
    (@ejgallego, #106, fixes #54)
  • Show goals on click by default, allow users to configure the
    behavior to follow cursor in different ways (@ejgallego, #116,
    fixes #89)
  • Show file position in goal buffer, use collapsible elements for
    goal list (@ejgallego, #115, fixes #109)
  • Resume checking from common prefix on document update (@ejgallego,
    #111, fixes #110)
  • Only serve goals, hover, and symbols requests when the document
    has been sufficiently processed (@ejgallego, #120, fixes #100)

Kind regards,
The coq-lsp team

[1] coq-lsp/ at main · ejgallego/coq-lsp · GitHub
[3] Coq Lsp Calls · ejgallego/coq-lsp Wiki · GitHub

Errata for the 0.1.0 release mail: we forgot Vincent Laporte in the list of contributors, who contributed the first version of the VSCode client. Thanks Vincent and sorry!

Please note that the coq-lsp 0.1.2 release in opam supports Coq 8.16. For advanced users, a version for the 8.17 release candidate can be found in our extra-dev Coq opam repo - please first add the core-dev opam repo to get access to the Coq release candidate.

1 Like