Releases: rocq-prover/vsrocq
v2.3.4
What's Changed
- Fix CI badge links in README.md by @gares in #1170
- Adapt to rocq-prover/rocq#20606 (some flags moved) by @SkySkimmer in #1086
- Adapt to rocq-prover/rocq#21281 (printing flags passed functionally) by @SkySkimmer in #1178 fgdgfdx
- Support
_RocqProjectby @simon-dima in #1179 - Document Manager: do not crash on outdated SeendProofView event by @gares in #1172
- Remove duplicate flake-utils in flake by @George-Miao in #1177
- Make goals.ppmode JSON key optional by @simon-dima in #1175
- Fix typo by @simon-dima in #1174
- Release 2.3.4 by @gares in #1180
New Contributors
- @simon-dima made their first contribution in #1179
- @George-Miao made their first contribution in #1177
Full Changelog: v2.3.3...v2.3.4
Contributors
Assets 3
v2.3.3
What's Changed
- Add vcoq-language-server.opam to publish commands by @gares in #1162
- Fix minor typos/stale links in github issue templates by @JoJoDeveloping in #1165
- make maintenance explicit in opam file by @gares in #1166
- Update conflict version for vscoq-language-server by @gares in #1167
- disable diff mode since it is broken by @gares in #1168
- bump version by @gares in #1169
Full Changelog: v2.3.2...v2.3.3
Contributors
Assets 3
v2.3.2
What's Changed
- Support Rocq 9.1.0 by @gares in #1156
- Update Readme for VsRocq by @JoJoDeveloping in #1159
- nix-ci runs fatalwarnings profile on rocq master only on linux by @gares in #1161
- bump version by @gares in #1160
New Contributors
- @JoJoDeveloping made their first contribution in #1159
Full Changelog: v2.3.1...v2.3.2
Contributors
Assets 3
v2.3.1
What's Changed
- Fix cd by @gares in #1145
- Update vscoq-language-server.opam by @patrick-nicodemus in #1149
- Release 2.3.1 by @gares in #1153
New Contributors
- @patrick-nicodemus made their first contribution in #1149
Full Changelog: v2.3.0...v2.3.1
Contributors
Assets 3
v2.3.0
This release renames the language server and extension to vsrocq
What's Changed
- fix: updated opam contraints by @rtetley in #1104
- Rename extension by @rtetley in #1078
- fix: opam file syntax error by @rtetley in #1105
- #1093: Renaming: vsrocq -> prover by @g0byx3 in #1110
- Add match! keywords for Ltac2 to syntax highligthing by @thomas-lamiaux in #1107
- Improve Makefile by @eponier in #1112
- Cherrypick fixes by @rtetley in #1120
- feat: add vscode and OS info to show setup command by @rtetley in #1124
- Adding FAQ and Issue Templates by @Durbatuluk1701 in #1121
- fix: rocq version display by @rtetley in #1126
- fix: forgot two cases for rocq version display by @rtetley in #1127
- Update README.md -> add nixos install by @srhhma in #1131
- feat: add an option to render goal view as formatted string + add range by @rtetley in #1133
- Fix 1066 by @gares in #1134
- fix: update the flake and CI by @rtetley in #1128
- Adapt to rocq-prover/rocq#20917 (changed with_end_tac arg in comtactic) by @SkySkimmer in #1135
- Adapt to rocq-prover/rocq#20962 (LStream.next returns option) by @SkySkimmer in #1136
- Adapt to rocq-prover/rocq#20997. by @ppedrot in #1139
- Adapt to rocq-prover/rocq#21020. by @ppedrot in #1140
- Adapt to rocq-prover/rocq#20964 (less exn driven parser) by @SkySkimmer in #1143
- release by @gares in #1144
New Contributors
Full Changelog: v2.2.6...v2.3.0
Contributors
Assets 3
v2.2.6
rtetley
Romain Tetley
What's Changed
Fixes
This release introduces a number of fixes. Most notably:
Execution bug
Before this fix, some tasks were executed twice
Problems with errored sentence in the diff and collisions in sentences map
Before this fix, two bad things would happen: the computed diff could be wrong which would cause havoc when re-parsing a document after an edit, and most notably, sometimes there were collisions in the sentences_by_end map which caused the document to be in an erroneous state (some sentences were recorded multiple times
Parsing events were not cancelled properly
The cancel handle was not passed properly in the state, this caused parsing events to happen multiple times and lead to poor performances as well as the infamous "reset" bug (see here)
Misc
Some other small bugs were fixed
- Ignore nested proofs option instead of failing with anomaly by @SkySkimmer in #1067
- Fix types of values sent to marshal by @SkySkimmer in #1082
- When moving to top end update_view and mk_proof_view events by @KacperFKorban in #1088
Minor changes
Outline
A number of minor improvements were made to the outline.
- feat: adding sections and modules in outlines by @rtetley in #1059
- Use all names from a vernac gen expr, when recording outline by @KacperFKorban in #1087
Syntax coloring
- Add highlighting for "Ltac2" by @thomas-lamiaux in #1075
- Add syntax highlighting for Ltac2 term definitions by @KacperFKorban in #1089
- syntax: add surrounding pairs to syntax support by @KacperFKorban in #1091
Visuals
In preparation for the renaming, the logos have been replaced
Full Changelog: v2.2.5...v2.2.6
Contributors
Assets 3
v2.2.5
rtetley
Romain Tetley
What's Changed
Fixes
Hotfix: server crashes when editing the file
A pernicious bug made it in the last release in which after executing through a parse error and then editing it, the server would crash.
This hotfix addresses this issue and is the main reason behind this small release.
Minor changes
Extension activation
The extension now only activates when a Coq file is opened ! This prevents annoying messages when a user is not trying to use Coq.
- Change activation to only occur when Coq files are opened by @Durbatuluk1701 in #1028
Better feedback performance
There has been an ongoing issue in which commands that generate feedback, such as Search, are unusable due to the time taken to handle the produced feedback. This feature greatly improves the situation and makes such commands usable again.
Don't crash for log messages
Sometimes producing log messages crashes the server. This ensures it won't happen again.
Symbol seaching and syntax highlighting
These changes add handling some keywords to the outline and fixes the syntax highlighting for others.
- syntax highlighting: Treat
Computeas a Vernacular keyword by @KacperFKorban in #1038 - Symbol search: handle inductive, fixpoint, and cofixpoint by @KacperFKorban in #1045
- syntax highlighting: support more vernacular commands by @KacperFKorban in #1047
New Contributors
- @KacperFKorban made their first contribution in #1038
Full Changelog: v2.2.4...v2.2.5
Contributors
Assets 3
v2.2.4
rtetley
Romain Tetley
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.
Color theme
A better color theme has been implemented making it so that warning messages are easy to read even in light mode:
- Set light and contrast theme colors for warning messages to amber by @Durbatuluk1701 in #1019
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:
- Return empty completions rather than error by @Durbatuluk1701 in #1012
Indentation
Improvements in the indentation behaviour were made:
- Change Language Config to Fix Indents by @Durbatuluk1701 in #1015
.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.
Full Changelog: v2.2.3...v2.2.4
Contributors
Assets 3
v2.2.3
rtetley
Romain Tetley
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:
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
Contributors
Assets 3
v2.2.2
rtetley
Romain Tetley
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 (rocq-prover/rocq#19584) so it will only be available on Coq dev and in the next version
of Rocq/Coq.
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.
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.
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.
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 (rocq-prover/rocq#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.
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
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
