Skip to content

v2.2.4

Compare
Choose a tag to compare
@github-actions github-actions released this 17 Feb 09:13
· 31 commits to main since this release
v2.2.4
fd598e6

What's Changed

This release contains a number of fixes.

Fixed

Block on parse error

Parse errors are now treated just like execution errors for block on first error mode.

Documentation

We now open the documentation for the installed coq version (rather than master):

Goal view

Some minor display issues due to some bugs in the pp format library were fixed.

  • fix: first box of a pp string was not processed by @rtetley in #984

Color theme

A better color theme has been implemented making it so that warning messages are easy to read even in light mode:

Step Through query commands

Query commands (such as Print, Search, ...) are now stepped through. This fixes a regression in continuous mode
where they were no longer displayed and some confusing coloring of the processed area:

Fix vscoqtop arguments

A regression in which arguments passed to vscoqtop were no longer read has been fixed:

No completions found

When no completions are found we send an empty list instead of an annoying error:

Indentation

Improvements in the indentation behaviour were made:

.vos files

We now load .vos files

Server crashes

We uncovered a problem in which parsing errors could lead to a server crash. This has been fixed.

Send proof view in continuous mode

A regression in continous mode (the proof view was no longer sent when reaching the cursor position) has been fixed.

  • Send a proof view in continuous mode when cursor position was executed by @rtetley in #1014

Full Changelog: v2.2.3...v2.2.4