package coq-lsp
Install
Dune Dependency
Authors
Maintainers
Sources
sha256=31b83f0908bbabf4079806ce9271a30f7af8fb4e2fd5c81c1ccc3c1e8022f0de
sha512=de9f48cb643944620183243a55a225b33b3b77d2cc2ea26e38377622ea9036e7205634e880d804dd0ae69ce22d321ce4dfbacc94aebb402d1f124d5be348ebca
CHANGES.md.html
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 ofcoq-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
orSearch
are not shown anymore as diagnostics. Instead, they will be shown on the side panel when clicking on the corresponding command. Theshow_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)