Need help with vscoq?
Click the “chat” button below for chat support from the developer who created it, or find similar developers for support.

About the developer

coq-community
132 Stars 22 Forks MIT License 645 Commits 61 Opened issues

Description

A Visual Studio Code extension for Coq [[email protected],@fakusb]

Services available

!
?

Need anything else?

Contributors list

# 109,180
coq
theorem...
OCaml
sed
52 commits
# 501,092
coq
theorem...
OCaml
sed
20 commits
# 37,680
real-ti...
mac
Windows
cmake
7 commits
# 16,346
Rust
tikz
coq
rfc
6 commits
# 455,100
coq
theorem...
OCaml
sed
4 commits
# 85,802
intelli...
jetbrai...
lean
vim-con...
3 commits
# 68,291
opam
jvm-lan...
agda
vlc
3 commits
# 93,935
coq
theorem...
depende...
sqlite3
2 commits
# 380,882
Shell
Haskell
colorsc...
termina...
2 commits
# 446,801
Gradle
HTML
coq
vscode
1 commit
# 392,406
Shell
Scala
formal-...
smt
1 commit
# 63,266
opam
coq
youtube...
currenc...
1 commit
# 98,632
coq
theorem...
OCaml
depende...
1 commit
# 341,407
coq
sed
depende...
latex-c...
1 commit
# 19,208
coq
LLVM
MATLAB
Node.js
1 commit
# 3,157
imagema...
sass-fr...
splash
pipelin...
1 commit

Travis Contributing Code of Conduct Zulip

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

This extension is currently developped 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.30.0 or more recent
  • Coq 8.7.0 or more recent

Installation

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

Screenshots

vscoq

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

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.

We use cookies. If you continue to browse the site, you agree to the use of cookies. For more information on our use of cookies please see our Privacy Policy.