[VsCoq 2] Release 2.1.7

Announcements
1

Hi everyone,

We are pleased to announce the next release of VsCoq. This release covers a number of fixes and new features. Some of these features were added in pre-releases (2.1.5, and 2.1.6) which we summarise here:

  • v2.1.5

    • Capabilities for quickfixes
      quickfix
      We have worked on adding quickfixes to VsCoq. However this relies on a change in the Coq API (which should send quickfix suggestions through warnings and errors). This change will only make it in the Coq 8.21 release.

    • Capabilities for outline
      outline
      We now support document outlines. At the moment we display definitions, theorems and such. We plan to add support for Modules and Sections in the future.

    • Memory management
      We have added a maximum memory setting. Upon reaching this limit, documents that have been closed in the editor will see their corresponding server states removed to save up space.

  • v2.1.6

    • Goal elliding
      goal-ellipsis
      For large goals, we have added an ellipsis mechanism. A user can first [alt+click] on any sub-term in the goal panel to elide/expand it. Additionally, there is now a setting accessible from the goals settings that will automatically trigger eliding when a goal is too large.

  • v2.1.7

    • Block on first error mode
      block-on-error
      Last but not least, we have added a block on first error mode. A user can opt out of “block on first error mode” through the user settings. Important: its is turned on by default, and this a behaviour change, particularly in continuous mode.

We would like to thank the Coq core developers as well as CodiePP (Alexander Diemand) · GitHub for their contributions to this release !

Stay tuned for more improvements !

Romain, for the VsCoq team.

5 Likes