package coq-lsp
Language Server Protocol native server for Coq
Install
Dune Dependency
Authors
Maintainers
Sources
coq-lsp-0.1.1.v8.16.tbz
sha256=be48fd1449d8a0eb209e83ebbcde95090e94ba74ee7e744a399c3a5b67cc4acb
sha512=c711b953346d3e45ed61c75d5f3825d877820dec38e5dc803cd1ab9a32d6b4a850232a84984c3c340d3939c459ea0595f606d303e1ba714e4245a784b3507ab0
doc/CHANGES.html
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)
sectionYPositions = computeSectionYPositions($el), 10)"
x-init="setTimeout(() => sectionYPositions = computeSectionYPositions($el), 10)"
>