Awesome
<!-- [![Travis][travis-shield]][travis-link] --> <!-- [![Available on the Visual Studio marketplace][vs-marketplace-shield]][vs-marketplace-link] [![Available on the Open VSX marketplace][open-vsx-shield]][open-vsx-link] --> <!-- [travis-shield]: https://travis-ci.com/coq-community/vscoq.svg?branch=master [travis-link]: https://travis-ci.com/coq-community/vscoq-legacy/builds --> <!-- [vs-marketplace-shield]: https://img.shields.io/visual-studio-marketplace/v/coq-community.vscoq1?label=Visual%20Studio%20Marketplace [vs-marketplace-link]: https://marketplace.visualstudio.com/items?itemName=coq-community.vscoq1 [open-vsx-shield]: https://img.shields.io/open-vsx/v/coq-community/vscoq1 [open-vsx-link]: https://open-vsx.org/extension/coq-community/vscoq1 -->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
- Works with prettify-symbols-mode
- Supports _CoqProject
- LtacProf results treeview
- Display type or notation definition on mouse hover.
Requirements
- VS Code or VSCodium 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
- install Coq
- install VS Code or VSCodium
- run
code
orcodium
- install this extension: press
F1
to open the command palette, start typing "Extensions: Install Extension", pressenter
, and search forvscoq1
- select "enable" on the extension
Basic usage
- if you use
_CoqProject
- start vscode viacode my/project/root
(orcode .
from the root folder of your project), or else select File|Open Folder... from vscode's menu. - step forward:
alt+down
(MacOS:Control+Option+down
) - step backward:
alt+up
(MacOS:Control+Option+up
) - interpret to point:
alt+right
(MacOS:Control+Option+right
) - interpret to end:
alt+end
(MacOS:Control+Option+End
) - reset (interpret to home):
alt+home
(MacOS:Control+Command+Home
) - explore more commands:
F1
and begin typingCoq:
- VS Code 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 tofalse
to ignore <span>_CoqProject</span>"coqtop.coqProjectRoot": "."
-- where to expect the <span>_CoqProject</span> 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.