VOOZH about

URL: https://marketplace.visualstudio.com/items?itemName=coq-community.vscoq1

⇱ VsCoq Legacy - Visual Studio Marketplace

Skip to content
👁 Image
| Marketplace
Sign in
Visual Studio Code>Programming Languages>VsCoq LegacyNew to Visual Studio Code? Get it now.
👁 VsCoq Legacy

VsCoq Legacy

An IDE for the Coq Proof Assistant
Installation
Launch VS Code Quick Open (Ctrl+P), paste the following command, and press enter.
Copied to clipboard
More Info

👁 Contributing
👁 Code of Conduct
👁 Zulip

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

👁 vscoq

Instructions

  1. install Coq
  2. install VS Code or VSCodium
  3. run code or codium
  4. install this extension: press F1 to open the command palette, start typing "Extensions: Install Extension", press enter, and search for vscoq1
  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 (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 typing Coq:
  • 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 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.