VsCoq 1 is an extension for Visual Studio Code (VS Code)
and VSCodium with support for the Coq Proof Assistant.
It is a legacy version compatible with Coq 8.17 or lower. If you are using Coq 8.18 or higher please use the VsCoq extension.
This extension is currently developed by @maximedenes and contributors, as
part of Coq Community. The
original author of this extension is @siegebell.
Features
Asynchronous proofs
Syntax highlighting
Commands: step forward, interpret to point, interrupt computation, queries, set display options, etc.
Diff view for proof-view: highlight which terms change between states
Smarter editing: does not roll back the state when editing whitespace or comments
install this extension: press F1 to open the command palette, start typing "Extensions: Install Extension", press enter, and search for vscoq1
select "enable" on the extension
Basic usage
if you use _CoqProject - start vscode via code my/project/root (or code . from the root folder of your project), or else select File|Open Folder... from vscode's menu.
(Press F1 and start typing "settings" to open either workspace/project or user settings.)
"coqtop.binPath": "" -- specify the path to coqtop (e.g. "path/to/coq/bin/")
"coqtop.args": [] -- an array of strings specifying additional command line arguments for coqtop
"coqtop.loadCoqProject": true -- set to false to ignore _CoqProject
"coqtop.coqProjectRoot": "." -- where to expect the _CoqProject relative to the workspace root
Install a local version
Checkout the repo, run make, and install the produced .vsix file in the repository root by following https://code.visualstudio.com/docs/editor/extension-gallery#_install-from-a-vsix. So, either "Cmd-Shift-P" and "Extensions: Install from VSIX", or running code --install-extension vscoq1-0.4.0.vsix (or whatever version number) from the terminal.
