23 Sep 08:33

f13ff1a

v2.2.1 Latest

Latest

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

Contributors

rtetley and Durbatuluk1701

Assets 3

06 Sep 14:39

github-actions

v2.2.0

6cc4d1d

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

Contributors

TDiazT, rtetley, and Durbatuluk1701

Assets 3

06 Aug 13:21

github-actions

v2.1.7

0b17857

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

Contributors

gares, SkySkimmer, and 3 other contributors

Assets 3

19 Jul 14:58

github-actions

v2.1.6

3f8f364

v2.1.6 Pre-release

Pre-release

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

Contributors

rtetley

Assets 3

15 Jul 11:15

github-actions

v2.1.5

108ffbe

v2.1.5 Pre-release

Pre-release

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

Contributors

rtetley

Assets 3

04 Jul 05:26

github-actions

v2.1.4

93d07e6

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

Contributors

gares, rlepigre, and 3 other contributors

Assets 3

14 Jun 13:17

github-actions

v2.1.3

8cdb3e6

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