package coq-lsp

  1. Overview
  2. Docs
Language Server Protocol native server for Coq

Install

Dune Dependency

Authors

Maintainers

Sources

coq-lsp-0.1.3.v8.16.tbz
sha256=d6d589ae18453d9251b4250df50e59cfc87254de0e4734e13c5bca06ab14cee5
sha512=802b4673c7f581976526a3cb4bd824f7574c5b1cc8fcc7759fcd3358cdc3e4cebef3ec908899ad68129190777ccda931dfc1643b45db156ede15acae0382c148

CHANGES.md.html

coq-lsp 0.1.3: Event

  • Much improved handling of Coq fatal errors, the server is now hardened against them (@ejgallego, #155, #157, #160, fixes #91)

  • coq-lsp now follows the LSP specification regarding initialization strictly (@ejgallego, #168)

  • New setting for goals to be updated when the selection changes due to a command; this makes VsCodeVim cursor tracking work; thanks to Cactus (Anton) Golov for detailed bug reporting and testing (@ejgallego, @jesyspa, #170, fixes #163)

  • coq-lsp will now warn the user when two files have been opened simultaneously and the parser may go into a broken state :/ (@ejgallego, #169)

  • Implement request postponement and cancellation. Thus documentSymbols will now be postponed until the document is ready, (@ejgallego, #141, #146, fixes #124)

  • Protocol and VS Code interfaces now support shelved and given_up goals (@ejgallego, #175)

  • Allow to postpone requests to wait for data to become available on document points; this is implemented to provide a nicer "show goals while I type" experience. Client default has been changed to "show goals on mouse, click, typing, and cursor movement) (@ejgallego, #177, #179)

  • Store stats per document (@ejgallego, #180, fixes #173)

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)

coq-lsp 0.1.0: Memory

  • Location-aware cache for incremental Coq interpretation (@ejgallego)

  • Smart, structure-aware error recovery (@ejgallego)

  • Configure flags reading _CoqProject file (@artagnon, #3)

  • Interruption support (@ejgallego , @Alizter, #27, #32, #34)

  • Markdown support (@ejgallego, #62)

  • Goal display (@ejgallego @corwin-of-amber, #69)

  • User-side configuration (@ejgallego, #67)

  • Allow to configure before/after goal display (@ejgallego, #78)

  • Allow requests to interrupt checking (@ejgallego, #76)

coq-lsp 0.0.0.1

  • Bootstrap from lambdapi-lsp server (@ejgallego)