-
Notifications
You must be signed in to change notification settings - Fork 35
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
[code] Improve client README and changelog.
- Loading branch information
Showing
2 changed files
with
30 additions
and
7 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -1,12 +1,34 @@ | ||
# Coq LSP VSCode client | ||
# Welcome to coq-lsp, a Language Server Protocol-based extension for the Coq Interactive Proof Assistant | ||
|
||
This is an experimental, pure-LSP client for Coq. | ||
`coq-lsp` aims to provide a modern and streamlined experience for | ||
VSCode users, relying on the new [coq-lsp language | ||
server](https://github.com/ejgallego/coq-lsp). | ||
|
||
You will need to install the server: | ||
The server provides many nice features such as incremental checking, | ||
advanced error recovery, document information, ... See the server | ||
documentation for more information. | ||
|
||
## Features | ||
|
||
The `coq-lsp` VSCode extension relies on the standard VSCode LSP | ||
client by Microsoft, with 2 main addons: | ||
|
||
- information / goal panel: this will display goals, messages, and | ||
errors at point. It does also support client-side rendering. By | ||
default, Cmd-Enter and mouse click will enable the panel for the | ||
current point. | ||
- document checking progress, using the right lane decoration. | ||
|
||
See the extension configuration options for more information. | ||
|
||
## How to install the server: | ||
|
||
To install the server please do: | ||
|
||
``` | ||
opam install coq-lsp | ||
``` | ||
|
||
Only Linux and OSX are supported for now; Windows support is hopefully | ||
coming soon. | ||
The server should also appear in the Coq Platform, and likely by other | ||
channels. | ||
|