vscoq

vscoq copied to clipboard

VsCoq is an extension for Visual Studio Code with support for the Coq Proof Assistant.

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
• Works with prettify-symbols-mode
• Supports _CoqProject
• LtacProf results treeview

Requirements

• VsCode 1.38.0 or more recent
• Coq 8.7.0 or more recent

Installation

The recommended way to install VsCoq is via the Visual Studio Marketplace or Open VSX .

Screenshots

Instructions

1. install Coq
2. install vscode
3. run code
4. install this extension: press F1 to open the command palette, start typing "Extensions: Install Extension", press enter, and search for vscoq
5. 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.
• step forward: alt+down
• step backward: alt+up
• interpret to point: alt+right
• interpret to end: alt+end
• interpret to home: alt+home
• explore more commands: F1 and begin typing Coq:
• vscode documentation

Settings

(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 vscoq-0.3.2.vsix (or whatever version number) from the terminal.