VsCoq is an extension for Visual Studio Code (VS Code) and VSCodium with support for the Coq Proof Assistant.
This extension is currently developed as part of Coq Community by Maxime Dénès, Enrico Tassi, Romain Tetley, and contributors.
This branch contains the VsCoq 2 language server and extension. It is a full reimplementation (based on a different architecture and design) of a previous version of VsCoq, whose original author was @siegebell. See the VsCoq 1 branch for the version of VsCoq that is on the Market Place.
VsCoq 2 is under heavy development and not ready for production use yet. It is not yet released nor published on the VsCode marketplace.
- Syntax highlighting
- Asynchronous proof checking
- Continuous and incremental checking of Coq documents
The new version of vscoq allows for continuous checking, see the goal panel update as you scroll or edit your document.
Note that users can opt out and choose to use the classic step by step checking mode.
- Customisable goal panel
Users can choose their preferred display mode, see goals in accordion lists...
... Or organized in tabs.
- Dedicated panel for queries and their history
We now support a dedicated panel for queries. We currently support Search, Check, About, Locate and Print with plans
to add more in the future.
- Supports _CoqProject
- VS Code or VSCodium 1.38.0, or more recent
- VsCoq 2 currently ships with a custom Coq version, and will later require Coq 8.18
(Press F1 and start typing "settings" to open either workspace/project or user settings.)
"vscoq.path": ""-- specify the path tovscoqtop(e.g.path/to/vscoq/bin/vscoqtop)"vscoq.args": []-- an array of strings specifying additional command line arguments forvscoqtop(typically accepts the same flags ascoqtop)
Unless mentioned otherwise, files in this repository are distributed under the MIT License.
The files client/syntax/coq.tmLanguage and client/coq.configuration.json are
also distributed under the MIT License, Copyright (c) Christian J. Bell and
contributors.