Skip to content

Latest commit

 

History

History
77 lines (56 loc) · 3.37 KB

README.md

File metadata and controls

77 lines (56 loc) · 3.37 KB
Raw

CI Contributing Code of Conduct Zulip

VsCoq is an extension for Visual Studio Code (VS Code) and VSCodium with support for the Coq Proof Assistant.

This extension is currently developed as part of Coq Community by Maxime Dénès, Enrico Tassi, Romain Tetley, and contributors.

This branch contains the VsCoq 2 language server and extension. It is a full reimplementation (based on a different architecture and design) of a previous version of VsCoq, whose original author was @siegebell. See the VsCoq 1 branch for the version of VsCoq that is on the Market Place.

Status

VsCoq 2 is under heavy development and not ready for production use yet. It is not yet released nor published on the VsCode marketplace.

Features

  • Syntax highlighting
  • Asynchronous proof checking
  • Continuous and incremental checking of Coq documents

The new version of vscoq allows for continuous checking, see the goal panel update as you scroll or edit your document.

Note that users can opt out and choose to use the classic step by step checking mode.

  • Customisable goal panel

Users can choose their preferred display mode, see goals in accordion lists...

... Or organized in tabs.

  • Dedicated panel for queries and their history

We now support a dedicated panel for queries. We currently support Search, Check, About, Locate and Print with plans to add more in the future.

  • Supports _CoqProject

Requirements

  • VS Code or VSCodium 1.38.0, or more recent
  • VsCoq 2 currently ships with a custom Coq version, and will later require Coq 8.18

Settings

(Press F1 and start typing "settings" to open either workspace/project or user settings.)

  • "vscoq.path": "" -- specify the path to vscoqtop (e.g. path/to/vscoq/bin/vscoqtop)
  • "vscoq.args": [] -- an array of strings specifying additional command line arguments for vscoqtop (typically accepts the same flags as coqtop)

License

Unless mentioned otherwise, files in this repository are distributed under the MIT License.

The files client/syntax/coq.tmLanguage and client/coq.configuration.json are also distributed under the MIT License, Copyright (c) Christian J. Bell and contributors.