Release of VSCoq 0.3.4 IDE

We’d like to announce the most recent release of VSCoq 0.3.4, the extension adding Coq support to the Visual Studio Code IDE.

The new version fixes several usability bugs (unreadable narrow proof views, bad performance in huge files of over 3000 lines and some other glitches that were only fixed by restarting) and improves several other aspects, see changelog.

We of course still have all the other features that make this a full-fledged Coq IDE:

  • 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

For me, the most important features of VSCoq are the support of asynchronous proof processing, the integration into the powerful VSCode extension ecosystem and the good performance when working on large files.

Feel free to comment on the Zulip chat or report bugs on Github.

3 Likes