v2.2.3

What's Changed

This is a release that contains a hot-fix for the vscoq-version-parser which allows us to use several lsp versions.
The aforementioned bug means we could not release 2.2.2. This version supersedes it.

The hotfix in question:

• version_parser: tolerate + in version numbers and never fail by @gares in #982

A fix was also added for finding vscoqtop path in windows.

• Replaced custom searchForVscoqtopInPath code with which by @cas-haaijman in #978

New Contributors

• @cas-haaijman made their first contribution in #978

Full Changelog: v2.2.2...v2.2.3

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

v2.2.1

What's Changed

Added

Better pretty printing library

The library we built to pretty print terms has been considerably improved. Drawing from Oppen's algorithm we are now much faster at displaying goals

• feat: optimize pp-display for a better and faster goal view and query panel by @rtetley in #900

This lays for the groundwork for further optimisations.

New options

Two new options have been introduced thanks to @Durbatuluk1701:

• vscoq.proof.display-buttons provides a way to disable the proof navigation and general buttons from the buffer
  
  feat: add config option to control whether Coq buttons are displayed by @Durbatuluk1701 in #904
• vscoq.proof.pointInterpretationMode determines the behaviour of the interpret to mode command, does it consider the sentence under the cursor or not ?
  "vscoq.proof.pointInterpretationMode" === Cursor

"vscoq.proof.pointInterpretationMode" === NextCommand
  
  feat: adding option for interpreting to exact cursor position or next command during interpret to point by @Durbatuluk1701 in #875

Prompt queries

The query actions now open a prompt window, if the cursor is pointing at a word, it pre-fills the prompt with the given word.

• feat: query actions are now done with prompts by @rtetley in #902

Show unfocused goals

Finally this release introduces the ability to view unfocused goals.

• feat: show message when goals are unfocused by @rtetley in #901

Fixed

Better hover

A number of fixes were introduced for hovers. We now differentiate between modules and their components. We also can over hover words containing '

• fix: hover for period qualifiers and single quotes in names by @Durbatuluk1701 in #899
• fix: off by one error in Hover by @Durbatuluk1701 in #903

Activity bar logo display

Finally, the VsCoq activity bar now only appears when there are coq files present in the workspace

• fix: make VsCoq activity bar logo appear only when Coq files present by @Durbatuluk1701 in #897

Goal view fixes

Note that the previously introduced improvements to pretty printing also solved a number of printing bugs such as printing inductive types.

Misc

• build: we only support 64 bit arch by @rtetley in #893

New contributors

No new contributors for this release.

Full Changelog: v2.2.0...v2.2.1

v2.2.0

What's Changed

Added

Query Panel results formatting

After externalising our lib to display PpStrings, we now support formatting in the query panel as well as in the goal panel.
Look forward to more improvements for the display of PpStrings soon

• feat: externalize pp-display library by @rtetley in #860* Update documentation by @rtetley in #856
• Search UI formatting by @rtetley in #861

New buttons and a menu

We have added the coq commands (in manual mode) as buttons accessible on top of the buffer.
On top of that we have added a main menu to access trouble shooting commands and documentation. This can be a building block for other neat features.

• feat: add buttons for the common coq navigation commands by @rtetley in #865
• feat: add a a main menu by @rtetley in #867
• feat: adding alt + shift click to expand all ellipsis goals by @Durbatuluk1701 in #871

A walkthrough

To improve the onboarding experience, we have added a walkthrough that is available at all times through the Coq: Docs: Show Setup Guide command as well as through the main menu described earlier

• feat: add a walkthrough by @rtetley in #868

Opt out of auto displaying goals

Finally, users can now opt out of the auto display of goals when running through a proof. The proof view is then accessible through the Coq: Display Proof View command, or the corresponding button in the new coq buttons row described earlier.

• feat: Disable the auto display for the proof view by @rtetley in #887

Bug fixes

Thanks to @Durbatuluk1701 for fixing a bug in which feedback messages were displayed the wrong way around.

• Changing feedback messages to be appended by @Durbatuluk1701 in #874

Misc

A formatter was added for the typscript code and the documentation and changelog were updated. The changelog of the extension now points to this page.

• config: Add prettier formatter by @TDiazT in #849
• docs: update change log by @rtetley in #885

New Contributors

• @TDiazT made their first contribution in #849

Full Changelog: v2.1.7...v2.2.0

v2.1.7

What's Changed

• [parser] use the loc of the prev sentence to feed the parser by @gares in #824
• [outline] list alien, named, symbols by @gares in #832
• Don't error on deprecated warnings in ocaml code by @SkySkimmer in #841
• allows newer ppx_yojson_conf version by @CodiePP in #833
• Get all debug messages by @rtetley in #842
• More complete document state request by @rtetley in #844
• Fix fatal warnings by @rtetley in #848
• Fix max depth setting initialization by @rtetley in #847
• [CI] test coq 8.20 by @gares in #807
• Fix client tests by @rtetley in #850
• Support block on first error mode by @rtetley in #845
• Work on better system for goal ellipsis by @thery in #846
• Correct unshelve message by @rtetley in #854

New Contributors

• @CodiePP made their first contribution in #833

Full Changelog: v2.1.6...v2.1.7

v2.1.6

What's Changed

• Update doc. Tweak ci. by @rtetley in #827
• Fix highlight bug by @rtetley in #828
• Stop recomputing display for big goals by @rtetley in #829
• Change default value for vscoq.goals.messages.full to true by @rtetley in #831
• Ellipsis by @rtetley in #834
• Remove display goals from package.json by @rtetley in #840

Full Changelog: v2.1.5...v2.1.6

v2.1.5

What's Changed

• Add options to publish-extension action. by @rtetley in #823
• Remove document from state table when it is closed. by @rtetley in #753
• Quickfix by @rtetley in #780
• Fix highlights by @rtetley in #805
• Capabilities for outline by @rtetley in #795

Full Changelog: v2.1.4...v2.1.5

v2.1.4

What's Changed

• Adapt to coq/coq#18973. by @rlepigre in #778
• adapt to coq/coq#19147 by @gares in #793
• Use set timeout to fix goal scrolling. by @rtetley in #798
• Fix pp display by @rtetley in #804
• fixup #775 by @gares in #781
• Fix errors when recovering from interp-error by @rtetley in #801
• Quickfix are in coq 8.21 by @FissoreD in #806
• Readme updates for default proof mode Manual and typos by @Durbatuluk1701 in #808

New Contributors

• @rlepigre made their first contribution in #778
• @FissoreD made their first contribution in #806
• @Durbatuluk1701 made their first contribution in #808

Full Changelog: v2.1.3...v2.1.4

v2.1.3

What's Changed

• Fix issue with build using flake system in issue #747 by @redanaheim in #754
• Improve flake.nix, add compatibility with pkgs.vscode extensions field by @redanaheim in #760
• Adapt to coq/coq#18422 (indirect accessor handled through vernactypes) by @SkySkimmer in #756
• Correct query panel bug by @rtetley in #763
• package.json: fix typo ("on after" => "one after") by @JasonGross in #764
• Fixed some typos in the settings. by @nbrader in #765
• Parsing comments by @rtetley in #755
• [coq] Adapt to coq/coq#18890 by @ejgallego in #767
• Fixed the optcomp keywords and functions by @rtetley in #769
• Add Equations and Equations? to coq.tmLanguage.json to get coloring by @thomas-lamiaux in #771
• Formatting proof view by @rtetley in #773
• Better highlights by @rtetley in #744
• [coq] Adapt to coq/coq#17393 by @ejgallego in #775
• Adding a warning as errors job in CI by @rtetley in #782
• [coq] Adapt to coq/coq#19187 by @ejgallego in #783
• Making manual mode the default one by @rtetley in #788
• Fix highlights by @rtetley in #786

New Contributors

• @redanaheim made their first contribution in #754
• @JasonGross made their first contribution in #764
• @nbrader made their first contribution in #765
• @ejgallego made their first contribution in #767
• @thomas-lamiaux made their first contribution in #771

Full Changelog: v2.1.2...v2.1.3

v2.1.2

What's Changed

• Adapt w.r.t. coq/coq#18652. by @ppedrot in #722
• Fix coq-master CI by @rtetley in #738
• Manual nav fix by @rtetley in #740
• Capture the correct loc for when an import fails. by @rtetley in #739

Full Changelog: v2.1.1+coq8.19...v2.1.2