Skip to content

Commit

Permalink
[code] Improve client README and changelog.
Browse files Browse the repository at this point in the history
  • Loading branch information
ejgallego committed Jan 8, 2023
1 parent 8a1ab0d commit 6d403d8
Show file tree
Hide file tree
Showing 2 changed files with 30 additions and 7 deletions.
5 changes: 3 additions & 2 deletions editor/code/CHANGELOG.md
Original file line number Diff line number Diff line change
@@ -1,12 +1,13 @@
# coq-lsp 0.1.2:
----------------
# coq-lsp 0.1.2: Message
------------------------

- Requires coq-lsp server 0.1.2, see full changelog at
https://github.com/ejgallego/coq-lsp/releases/tag/0.1.2
- Extension will now enforce that server has the correct version
- The Coq LSP server output window will now show trace information
- Coq Info Panel will now show messages coming from commands such as
`About` or `Search`
- Coq Info Panel will now show detailed error information.

# coq-lsp 0.1.1: Location
-------------------------
Expand Down
32 changes: 27 additions & 5 deletions editor/code/README.md
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.

0 comments on commit 6d403d8

Please sign in to comment.