v2.2.2

What's Changed

Important information

Due to a unforeseen problem when running the opam CI, we could not release 2.2.2, we immediately released 2.2.3 with a hotfix.

Added

Jump to definition

We have introduced jump to definition capabilities. Note this required some changes in Rocq/Coq (coq/coq#19584) so it will only be available on Coq dev and in the next version
of Rocq/Coq.

• feat: jump to definition proof of concept by @rtetley in #911

Better goal display readibility

When there are multiple goals in list mode, we now only display the goal context for the first goal.
We also add a button allowing to hide/show the goal context.

• Remove hypothesis display from goal list by @rtetley in #962

External API

This release introduces an external API, allowing developers to depend on VsCoq with their own vscode extension and gain access to this API.
Here we introduce a function which allows for an external extension to get all the proofs contained in a document.

    vscoq = extensions.getExtension('maximedenes.vscoq');
    const documentProofs = await vscoq?.exports.getDocumentProofs(document.uri);

You can expect to see more API points being added in the future.

• Get proof blocks api by @rtetley in #960

Organisation change

VsCoq is now part of the Rocq/Coq. VsCoq Legacy will stay part of coq-community.

• doc: update doc after organization change by @rtetley in #926
• README.md: link to separate repo for VsCoq Legacy by @Blaisorblade in #928

Documentation

• docs: add troubleshooting section to install instructions by @rtetley in #922
• Update developers.md with more info, allowing to use vscoq2 during de… by @mattam82 in #916

Fixed

Better cursor placement on error

In manual mode, if block on first error mode is activated, the cursor will be placed right after the error range, instead of the last
correct sentence.

• Place the cursor at the end of the error when block on error mode is active by @rtetley in #963

Better _CoqProject support

Before this change the _CoqProject file was only searched on launch, and we could not load it after.
Note that this required some changes in Coq/Rocq (coq/coq#19826) and will only be supported
with Coq/Rocq dev and the next version of Coq/Rocq.

• Support per-file _CoqProject by @SkySkimmer in #945

Better handling of events loop and parsing

As was noted, there have been some performance issues while editing Rocq/Coq files (#914).
This was due to the design of the parsing event, which was triggered everytime a modification was detected on a file, and for the full file
(i.e. each time a user typed something, a full parse of the document was launched).
Now each line has its independant parse event allowing us to cancel prior events and only parse the most recent version of the document.

• Cancel parsing event by @rtetley in #941

Some fixes to syntax highighting

• syntax: Add boundary conditions when matching keywords by @Lysxia in #927
• syntax: Highlight Goal in any context by @Lysxia in #935

Better error logging

• toplevel: always print fatal exception by @gares in #955
• Adding error codes and better logging by @rtetley in #957
• Fix incorrect reference to vscoq.trace.server by @cpitclaudel in #974

Misc fixes

• support lsp >= 1.19 by @gares in #970
• link LICENSE and README in client by @gares in #971

New Contributors

• @Lysxia made their first contribution in #927
• @mattam82 made their first contribution in #961
• @cpitclaudel made their first contribution in #974

Full Changelog: v2.2.1...v2.2.2