coq-lsp | VS Code Extension Ecosystem Directory

Bot releases are hidden (Show)

coq-lsp - 0.1.9+8.17 Latest Release

Published by ejgallego 5 months ago

CHANGES:

new option show_loc_info_on_hover that will display parsing debug
information on hover; previous flag was fixed in code, which is way
less flexible. This also fixes the option being on in 0.1.8 by
mistake (@ejgallego, #588)
hover plugins can now access the full document, this is convenient
for many use cases (@ejgallego, #591)
fix hover position computation on the presence of Utf characters
(@ejgallego, #597, thanks to Pierre Courtieu for the report and
example, closes #594)
fix activation bug that prevented extension activation for .mv
files, see discussion in the issues about the upstream policy
(@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman)
require VSCode >= 1.82 in package.json . Our VSCode extension uses
vscode-languageclient 9 which imposes this. (@ejgallego, #599,
thanks to Théo Zimmerman for the report)
proof/goals request: new mode parameter, to specify goals
after/before sentence display; renamed pretac to command, as to
provide official support for speculative execution (@ejgallego, #600)
fix some cases where interrupted computations where memoized
(@ejgallego, #603)
[internal] Flèche [Doc.t] API will now absorb errors on document
update and creation into the document itself. Thus, a document that
failed to create or update is still valid, but in the right failed
state. This is a much needed API change for a lot of use cases
(@ejgallego, #604)
support OCaml 5.1.x (@ejgallego, #606)
update progress indicator correctly on End Of File (@ejgallego,
#605, fixes #445)
[plugins] New astdump plugin to dump AST of files into JSON and
SEXP (@ejgallego, #607)
errors on save where not properly caught (@ejgallego, #608)
switch default of goal_after_tactic to true (@Alizter,
@ejgallego, cc: #614)
error recovery: Recognize Defined and Admitted in lex recovery
(@ejgallego, #616)
completion: correctly understand UTF-16 code points on completion
request (Léo Stefanesco, #613, fixes #531)
don't trigger the goals window in general markdown buffer
(@ejgallego, #625, reported by Théo Zimmerman)
allow not to postpone full document requests (#626, @ejgallego)
new configuration value check_only_on_request which will delay
checking the document until a request has been made (#629, cc: #24,
@ejgallego)
fix typo on package.json configuration section (@ejgallego, #645)
be more resilient with invalid _CoqProject files (@ejgallego, #646)
support for Coq 8.16 has been abandoned due to lack of dev
resources (@ejgallego, #649)
new option --no_vo for fcc, which will skip the .vo saving
step. .vo saving is now an fcc plugins, but for now, it is
enabled by default (@ejgallego, #650)
depend on memprof-limits on OCaml 4.x (@ejgallego, #660)
bump minimal OCaml version to 4.12 due to memprof-limits
(@ejgallego, #660)
monitor all Coq-level calls under an interruption token
(@ejgallego, #661)
interpret require thru our own custom execution env-aware path
(@bhaktishh, @ejgallego, #642, #643, #644)
new coq-lsp.plugin.goaldump plugin, as an example on how to dump
goals from a document (@ejgallego @gbdrt, #619)
new trim command (both in the server and in VSCode) to liberate
space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
#348)
fix Coq performance view display (@ejgallego, #663, regression in
#513)
Added new heatmap feature allowing timing data to be seen in the
editor. Can be enabled with the Coq LSP: Toggle heatmap
command. Can be configured to show memory usage. Colors and
granularity are configurable. (@Alizter and @ejgallego, #686,
grants #681).
allow more than one input position in selectionRange LSP call
(@ejgallego, #667, fixes #663)
new VSCode commands to allow to move one sentence backwards /
forward, this is particularly useful when combined with lazy
checking mode (@ejgallego, #671, fixes #263, fixes #580)
VSCode commands coq-lsp.sentenceNext / coq-lsp.sentencePrevious
are now bound by default to Alt + N / Alt + P keybindings
(@ejgallego, #718)
change diagnostic extra field to data, so we now conform to the
LSP spec, include the data only when the send_diags_extra_data
server-side option is enabled (@ejgallego, #670)
include range of full sentence in error diagnostic extra data
(@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #663).
The coq-lsp.pp_type VSCode client option now takes effect
immediately, no more need to restart the server to get different
goal display formats (@ejgallego, #675)
new public VSCode extension API so other extensions can perform
actions when the user request the goals (@ejgallego, @bhaktishh,
#672, fixes #538)
Support Visual Studio Live Share URIs better (vsls://), in
particular don't try to display goals if the URI is VSLS one
(@ejgallego, #676)
New InjectRequire plugin API for plugins to be able to instrument
the default import list of files (@ejgallego @corwin-of-amber,
#679)
Add --max_errors=n option to fcc, this way users can set
--max_errors=0 to imitate coqc behavior (@ejgallego, #680)
Fix fcc exit status when checking terminates with fatal errors
(@ejgallego, @Alizter, #680)
Fix install to OPAM switches from main branch (@ejgallego, #683,
fixes #682, cc #479 #488, thanks to @Hazardouspeach for the report)
New --int_backend={Coq,Mp} command line parameter to select the
interruption method for Coq (@ejgallego, #684)
Update package-lock.json for latest bugfixes (@ejgallego, #687)
Update Nix flake enviroment (@Alizter, #684 #688)
Update prettier (@Alizter @ejgallego, #684 #688)
Store original performance data in the cache, so we now display the
original timing and memory data even for cached commands (@ejgallego, #693)
Fix type errors in the Performance Data Notifications (@ejgallego,
@Alizter, #689, #693)
Send performance performance data for the full document
(@ejgallego, @Alizter, #689, #693)
Better types coq/perfData call (@ejgallego @Alizter, #689)
New server option to enable / disable coq/perfData (@ejgallego, #689)
New client option to enable / disable coq/perfData (@ejgallego, #717)
The coq-lsp.document VSCode command will now display the returned
JSON data in a new editor (@ejgallego, #701)
Update server settings on the fly when tweaking them in VSCode.
Implement workspace/didChangeConfiguration (@ejgallego, #702)
[Coq API] Add functions to retrieve list of declarations done in
.vo files (@ejallego, @eytans, #704)
New petanque API to interact directly with Coq's proof
engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to
Alex Sanchez-Stern for many insightful feedback and testing)
New petanque JSON-RPC pet.exe, which can be used à la SerAPI
to perform proof search and more (@ejgallego, @gbdrt, #705)
New pet-server.exe TCP server for keep-alive sessions (@gbdrt,
#697)
Always dispose UI elements. This should improve some strange
behaviors on extension restart (@ejgallego, #708)
[code] Added new heatmap feature allowing timing data to be seen in
the editor. Can be enabled with the Coq LSP: Toggle heatmap
comamnd. Can be configured to show memory usage. Colors and
granularity are configurable. (@Alizter and @ejgallego, #686,
grants #681).
[server] Support Coq meta-commands (Reset, Reset Initial, Back)
They are actually pretty useful to hint the incremental engine to
ignore changes in some part of the document (@ejgallego, #709)
JSON-RPC library now supports all kind of incoming messages
(@ejgallego, #713)
[code/server] New coq/viewRange notification, from client to
server, than hints the scheduler for the visible area of the
document; combined with the new lazy checking mode, this provides
checking on scroll, a feature inspired from Isabelle IDE
(@ejgallego, #717)
[code] Have VSCode wait for full LSP client shutdown on server
restart. This fixes some bugs on extension restart (finally!)
(@ejgallego, #719)
[code] Center the view if cursor goes out of scope in
sentenceNext/sentencePrevious (@ejgallego, #718)
Switch Flèche range encoding to protocol native, this means UTF-16
code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
#621)
Give Goals panel focus back if it has lost it (in case of
multiple panels in the second viewColumn of Vscode) whenever
user navigates proofs (@Alidra @ejgallego, #722, #725)
fcc: new option --diags_level to control whether Coq's notice
and info messages appear as diagnostics
[code] Display the continous/on-request checking mode in the status bar,
allow to change it by clicking on it (@ejgallego, #721)
Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
#611)
Don't show types of un-expanded goals. We should add an option for
this, but we don't have the cycles (@ejgallego, #730, workarounds
#525 #652)
Support for .lv / .v.tex TeX files with embedded Coq code
(@ejgallego, #727)
Don't expand bullet goals at previous levels by default
(@ejgallego, @Alizter, #731 cc #525)
[petanque] Return basic goal information after run_tac, so we
avoid a goals round-trip for each tactic (@gbdrt, @ejgallego,
#733)
[coq] Add support for reading glob files metadata (@ejgallego,
#735)
[petanque] Return extra premise information: file name, position,
raw_text, using the above support for reading .glob files
(@ejgallego, #735)
[code] Display server status using the LanguageStatusItem
facility, for now we display version and checking status
information (moved from #721), and we also allow to toggle the
checking mode from there (@ejgallego, #728)

coq-lsp - 0.1.9+8.18

Published by ejgallego 5 months ago

CHANGES:

new option show_loc_info_on_hover that will display parsing debug
information on hover; previous flag was fixed in code, which is way
less flexible. This also fixes the option being on in 0.1.8 by
mistake (@ejgallego, #588)
hover plugins can now access the full document, this is convenient
for many use cases (@ejgallego, #591)
fix hover position computation on the presence of Utf characters
(@ejgallego, #597, thanks to Pierre Courtieu for the report and
example, closes #594)
fix activation bug that prevented extension activation for .mv
files, see discussion in the issues about the upstream policy
(@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman)
require VSCode >= 1.82 in package.json . Our VSCode extension uses
vscode-languageclient 9 which imposes this. (@ejgallego, #599,
thanks to Théo Zimmerman for the report)
proof/goals request: new mode parameter, to specify goals
after/before sentence display; renamed pretac to command, as to
provide official support for speculative execution (@ejgallego, #600)
fix some cases where interrupted computations where memoized
(@ejgallego, #603)
[internal] Flèche [Doc.t] API will now absorb errors on document
update and creation into the document itself. Thus, a document that
failed to create or update is still valid, but in the right failed
state. This is a much needed API change for a lot of use cases
(@ejgallego, #604)
support OCaml 5.1.x (@ejgallego, #606)
update progress indicator correctly on End Of File (@ejgallego,
#605, fixes #445)
[plugins] New astdump plugin to dump AST of files into JSON and
SEXP (@ejgallego, #607)
errors on save where not properly caught (@ejgallego, #608)
switch default of goal_after_tactic to true (@Alizter,
@ejgallego, cc: #614)
error recovery: Recognize Defined and Admitted in lex recovery
(@ejgallego, #616)
completion: correctly understand UTF-16 code points on completion
request (Léo Stefanesco, #613, fixes #531)
don't trigger the goals window in general markdown buffer
(@ejgallego, #625, reported by Théo Zimmerman)
allow not to postpone full document requests (#626, @ejgallego)
new configuration value check_only_on_request which will delay
checking the document until a request has been made (#629, cc: #24,
@ejgallego)
fix typo on package.json configuration section (@ejgallego, #645)
be more resilient with invalid _CoqProject files (@ejgallego, #646)
support for Coq 8.16 has been abandoned due to lack of dev
resources (@ejgallego, #649)
new option --no_vo for fcc, which will skip the .vo saving
step. .vo saving is now an fcc plugins, but for now, it is
enabled by default (@ejgallego, #650)
depend on memprof-limits on OCaml 4.x (@ejgallego, #660)
bump minimal OCaml version to 4.12 due to memprof-limits
(@ejgallego, #660)
monitor all Coq-level calls under an interruption token
(@ejgallego, #661)
interpret require thru our own custom execution env-aware path
(@bhaktishh, @ejgallego, #642, #643, #644)
new coq-lsp.plugin.goaldump plugin, as an example on how to dump
goals from a document (@ejgallego @gbdrt, #619)
new trim command (both in the server and in VSCode) to liberate
space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
#348)
fix Coq performance view display (@ejgallego, #663, regression in
#513)
Added new heatmap feature allowing timing data to be seen in the
editor. Can be enabled with the Coq LSP: Toggle heatmap
command. Can be configured to show memory usage. Colors and
granularity are configurable. (@Alizter and @ejgallego, #686,
grants #681).
allow more than one input position in selectionRange LSP call
(@ejgallego, #667, fixes #663)
new VSCode commands to allow to move one sentence backwards /
forward, this is particularly useful when combined with lazy
checking mode (@ejgallego, #671, fixes #263, fixes #580)
VSCode commands coq-lsp.sentenceNext / coq-lsp.sentencePrevious
are now bound by default to Alt + N / Alt + P keybindings
(@ejgallego, #718)
change diagnostic extra field to data, so we now conform to the
LSP spec, include the data only when the send_diags_extra_data
server-side option is enabled (@ejgallego, #670)
include range of full sentence in error diagnostic extra data
(@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #663).
The coq-lsp.pp_type VSCode client option now takes effect
immediately, no more need to restart the server to get different
goal display formats (@ejgallego, #675)
new public VSCode extension API so other extensions can perform
actions when the user request the goals (@ejgallego, @bhaktishh,
#672, fixes #538)
Support Visual Studio Live Share URIs better (vsls://), in
particular don't try to display goals if the URI is VSLS one
(@ejgallego, #676)
New InjectRequire plugin API for plugins to be able to instrument
the default import list of files (@ejgallego @corwin-of-amber,
#679)
Add --max_errors=n option to fcc, this way users can set
--max_errors=0 to imitate coqc behavior (@ejgallego, #680)
Fix fcc exit status when checking terminates with fatal errors
(@ejgallego, @Alizter, #680)
Fix install to OPAM switches from main branch (@ejgallego, #683,
fixes #682, cc #479 #488, thanks to @Hazardouspeach for the report)
New --int_backend={Coq,Mp} command line parameter to select the
interruption method for Coq (@ejgallego, #684)
Update package-lock.json for latest bugfixes (@ejgallego, #687)
Update Nix flake enviroment (@Alizter, #684 #688)
Update prettier (@Alizter @ejgallego, #684 #688)
Store original performance data in the cache, so we now display the
original timing and memory data even for cached commands (@ejgallego, #693)
Fix type errors in the Performance Data Notifications (@ejgallego,
@Alizter, #689, #693)
Send performance performance data for the full document
(@ejgallego, @Alizter, #689, #693)
Better types coq/perfData call (@ejgallego @Alizter, #689)
New server option to enable / disable coq/perfData (@ejgallego, #689)
New client option to enable / disable coq/perfData (@ejgallego, #717)
The coq-lsp.document VSCode command will now display the returned
JSON data in a new editor (@ejgallego, #701)
Update server settings on the fly when tweaking them in VSCode.
Implement workspace/didChangeConfiguration (@ejgallego, #702)
[Coq API] Add functions to retrieve list of declarations done in
.vo files (@ejallego, @eytans, #704)
New petanque API to interact directly with Coq's proof
engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to
Alex Sanchez-Stern for many insightful feedback and testing)
New petanque JSON-RPC pet.exe, which can be used à la SerAPI
to perform proof search and more (@ejgallego, @gbdrt, #705)
New pet-server.exe TCP server for keep-alive sessions (@gbdrt,
#697)
Always dispose UI elements. This should improve some strange
behaviors on extension restart (@ejgallego, #708)
[code] Added new heatmap feature allowing timing data to be seen in
the editor. Can be enabled with the Coq LSP: Toggle heatmap
comamnd. Can be configured to show memory usage. Colors and
granularity are configurable. (@Alizter and @ejgallego, #686,
grants #681).
[server] Support Coq meta-commands (Reset, Reset Initial, Back)
They are actually pretty useful to hint the incremental engine to
ignore changes in some part of the document (@ejgallego, #709)
JSON-RPC library now supports all kind of incoming messages
(@ejgallego, #713)
[code/server] New coq/viewRange notification, from client to
server, than hints the scheduler for the visible area of the
document; combined with the new lazy checking mode, this provides
checking on scroll, a feature inspired from Isabelle IDE
(@ejgallego, #717)
[code] Have VSCode wait for full LSP client shutdown on server
restart. This fixes some bugs on extension restart (finally!)
(@ejgallego, #719)
[code] Center the view if cursor goes out of scope in
sentenceNext/sentencePrevious (@ejgallego, #718)
Switch Flèche range encoding to protocol native, this means UTF-16
code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
#621)
Give Goals panel focus back if it has lost it (in case of
multiple panels in the second viewColumn of Vscode) whenever
user navigates proofs (@Alidra @ejgallego, #722, #725)
fcc: new option --diags_level to control whether Coq's notice
and info messages appear as diagnostics
[code] Display the continous/on-request checking mode in the status bar,
allow to change it by clicking on it (@ejgallego, #721)
Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
#611)
Don't show types of un-expanded goals. We should add an option for
this, but we don't have the cycles (@ejgallego, #730, workarounds
#525 #652)
Support for .lv / .v.tex TeX files with embedded Coq code
(@ejgallego, #727)
Don't expand bullet goals at previous levels by default
(@ejgallego, @Alizter, #731 cc #525)
[petanque] Return basic goal information after run_tac, so we
avoid a goals round-trip for each tactic (@gbdrt, @ejgallego,
#733)
[coq] Add support for reading glob files metadata (@ejgallego,
#735)
[petanque] Return extra premise information: file name, position,
raw_text, using the above support for reading .glob files
(@ejgallego, #735)
[code] Display server status using the LanguageStatusItem
facility, for now we display version and checking status
information (moved from #721), and we also allow to toggle the
checking mode from there (@ejgallego, #728)

coq-lsp - 0.1.9+8.19

Published by ejgallego 5 months ago

CHANGES:

new option show_loc_info_on_hover that will display parsing debug
information on hover; previous flag was fixed in code, which is way
less flexible. This also fixes the option being on in 0.1.8 by
mistake (@ejgallego, #588)
hover plugins can now access the full document, this is convenient
for many use cases (@ejgallego, #591)
fix hover position computation on the presence of Utf characters
(@ejgallego, #597, thanks to Pierre Courtieu for the report and
example, closes #594)
fix activation bug that prevented extension activation for .mv
files, see discussion in the issues about the upstream policy
(@ejgallego @r3m0t, #598, cc #596, reported by Théo Zimmerman)
require VSCode >= 1.82 in package.json . Our VSCode extension uses
vscode-languageclient 9 which imposes this. (@ejgallego, #599,
thanks to Théo Zimmerman for the report)
proof/goals request: new mode parameter, to specify goals
after/before sentence display; renamed pretac to command, as to
provide official support for speculative execution (@ejgallego, #600)
fix some cases where interrupted computations where memoized
(@ejgallego, #603)
[internal] Flèche [Doc.t] API will now absorb errors on document
update and creation into the document itself. Thus, a document that
failed to create or update is still valid, but in the right failed
state. This is a much needed API change for a lot of use cases
(@ejgallego, #604)
support OCaml 5.1.x (@ejgallego, #606)
update progress indicator correctly on End Of File (@ejgallego,
#605, fixes #445)
[plugins] New astdump plugin to dump AST of files into JSON and
SEXP (@ejgallego, #607)
errors on save where not properly caught (@ejgallego, #608)
switch default of goal_after_tactic to true (@Alizter,
@ejgallego, cc: #614)
error recovery: Recognize Defined and Admitted in lex recovery
(@ejgallego, #616)
completion: correctly understand UTF-16 code points on completion
request (Léo Stefanesco, #613, fixes #531)
don't trigger the goals window in general markdown buffer
(@ejgallego, #625, reported by Théo Zimmerman)
allow not to postpone full document requests (#626, @ejgallego)
new configuration value check_only_on_request which will delay
checking the document until a request has been made (#629, cc: #24,
@ejgallego)
fix typo on package.json configuration section (@ejgallego, #645)
be more resilient with invalid _CoqProject files (@ejgallego, #646)
support for Coq 8.16 has been abandoned due to lack of dev
resources (@ejgallego, #649)
new option --no_vo for fcc, which will skip the .vo saving
step. .vo saving is now an fcc plugins, but for now, it is
enabled by default (@ejgallego, #650)
depend on memprof-limits on OCaml 4.x (@ejgallego, #660)
bump minimal OCaml version to 4.12 due to memprof-limits
(@ejgallego, #660)
monitor all Coq-level calls under an interruption token
(@ejgallego, #661)
interpret require thru our own custom execution env-aware path
(@bhaktishh, @ejgallego, #642, #643, #644)
new coq-lsp.plugin.goaldump plugin, as an example on how to dump
goals from a document (@ejgallego @gbdrt, #619)
new trim command (both in the server and in VSCode) to liberate
space used in the cache (@ejgallego, #662, fixes #367 cc: #253 #236
#348)
fix Coq performance view display (@ejgallego, #663, regression in
#513)
Added new heatmap feature allowing timing data to be seen in the
editor. Can be enabled with the Coq LSP: Toggle heatmap
command. Can be configured to show memory usage. Colors and
granularity are configurable. (@Alizter and @ejgallego, #686,
grants #681).
allow more than one input position in selectionRange LSP call
(@ejgallego, #667, fixes #663)
new VSCode commands to allow to move one sentence backwards /
forward, this is particularly useful when combined with lazy
checking mode (@ejgallego, #671, fixes #263, fixes #580)
VSCode commands coq-lsp.sentenceNext / coq-lsp.sentencePrevious
are now bound by default to Alt + N / Alt + P keybindings
(@ejgallego, #718)
change diagnostic extra field to data, so we now conform to the
LSP spec, include the data only when the send_diags_extra_data
server-side option is enabled (@ejgallego, #670)
include range of full sentence in error diagnostic extra data
(@ejgallego, #670 , thanks to @driverag22 for the idea, cc: #663).
The coq-lsp.pp_type VSCode client option now takes effect
immediately, no more need to restart the server to get different
goal display formats (@ejgallego, #675)
new public VSCode extension API so other extensions can perform
actions when the user request the goals (@ejgallego, @bhaktishh,
#672, fixes #538)
Support Visual Studio Live Share URIs better (vsls://), in
particular don't try to display goals if the URI is VSLS one
(@ejgallego, #676)
New InjectRequire plugin API for plugins to be able to instrument
the default import list of files (@ejgallego @corwin-of-amber,
#679)
Add --max_errors=n option to fcc, this way users can set
--max_errors=0 to imitate coqc behavior (@ejgallego, #680)
Fix fcc exit status when checking terminates with fatal errors
(@ejgallego, @Alizter, #680)
Fix install to OPAM switches from main branch (@ejgallego, #683,
fixes #682, cc #479 #488, thanks to @Hazardouspeach for the report)
New --int_backend={Coq,Mp} command line parameter to select the
interruption method for Coq (@ejgallego, #684)
Update package-lock.json for latest bugfixes (@ejgallego, #687)
Update Nix flake enviroment (@Alizter, #684 #688)
Update prettier (@Alizter @ejgallego, #684 #688)
Store original performance data in the cache, so we now display the
original timing and memory data even for cached commands (@ejgallego, #693)
Fix type errors in the Performance Data Notifications (@ejgallego,
@Alizter, #689, #693)
Send performance performance data for the full document
(@ejgallego, @Alizter, #689, #693)
Better types coq/perfData call (@ejgallego @Alizter, #689)
New server option to enable / disable coq/perfData (@ejgallego, #689)
New client option to enable / disable coq/perfData (@ejgallego, #717)
The coq-lsp.document VSCode command will now display the returned
JSON data in a new editor (@ejgallego, #701)
Update server settings on the fly when tweaking them in VSCode.
Implement workspace/didChangeConfiguration (@ejgallego, #702)
[Coq API] Add functions to retrieve list of declarations done in
.vo files (@ejallego, @eytans, #704)
New petanque API to interact directly with Coq's proof
engine. (@ejgallego, @gbdrt, Laetitia Teodorescu #703, thanks to
Alex Sanchez-Stern for many insightful feedback and testing)
New petanque JSON-RPC pet.exe, which can be used à la SerAPI
to perform proof search and more (@ejgallego, @gbdrt, #705)
New pet-server.exe TCP server for keep-alive sessions (@gbdrt,
#697)
Always dispose UI elements. This should improve some strange
behaviors on extension restart (@ejgallego, #708)
[code] Added new heatmap feature allowing timing data to be seen in
the editor. Can be enabled with the Coq LSP: Toggle heatmap
comamnd. Can be configured to show memory usage. Colors and
granularity are configurable. (@Alizter and @ejgallego, #686,
grants #681).
[server] Support Coq meta-commands (Reset, Reset Initial, Back)
They are actually pretty useful to hint the incremental engine to
ignore changes in some part of the document (@ejgallego, #709)
JSON-RPC library now supports all kind of incoming messages
(@ejgallego, #713)
[code/server] New coq/viewRange notification, from client to
server, than hints the scheduler for the visible area of the
document; combined with the new lazy checking mode, this provides
checking on scroll, a feature inspired from Isabelle IDE
(@ejgallego, #717)
[code] Have VSCode wait for full LSP client shutdown on server
restart. This fixes some bugs on extension restart (finally!)
(@ejgallego, #719)
[code] Center the view if cursor goes out of scope in
sentenceNext/sentencePrevious (@ejgallego, #718)
Switch Flèche range encoding to protocol native, this means UTF-16
code points for now (Léo Stefanesco, @ejgallego, #624, fixes #620,
#621)
Give Goals panel focus back if it has lost it (in case of
multiple panels in the second viewColumn of Vscode) whenever
user navigates proofs (@Alidra @ejgallego, #722, #725)
fcc: new option --diags_level to control whether Coq's notice
and info messages appear as diagnostics
[code] Display the continous/on-request checking mode in the status bar,
allow to change it by clicking on it (@ejgallego, #721)
Add an example of multiple workspaces (@ejgallego, @Blaisorblade,
#611)
Don't show types of un-expanded goals. We should add an option for
this, but we don't have the cycles (@ejgallego, #730, workarounds
#525 #652)
Support for .lv / .v.tex TeX files with embedded Coq code
(@ejgallego, #727)
Don't expand bullet goals at previous levels by default
(@ejgallego, @Alizter, #731 cc #525)
[petanque] Return basic goal information after run_tac, so we
avoid a goals round-trip for each tactic (@gbdrt, @ejgallego,
#733)
[coq] Add support for reading glob files metadata (@ejgallego,
#735)
[petanque] Return extra premise information: file name, position,
raw_text, using the above support for reading .glob files
(@ejgallego, #735)
[code] Display server status using the LanguageStatusItem
facility, for now we display version and checking status
information (moved from #721), and we also allow to toggle the
checking mode from there (@ejgallego, #728)

coq-lsp - 0.1.8+8.19

Published by ejgallego 9 months ago

CHANGES:

Update VSCode client dependencies, should bring some performance
improvements to goal pretty printing (@ejgallego, #530)
Update goal display colors for light mode so they are actually
readable now. (@bhaktishh, #539, fixes #532)
Added link to Python coq-lsp client by Pedro Carrot and Nuno
Saavedra (@Nfsaavedra, #536)
Properly concatenate warnings from _CoqProject (@ejgallego,
reported by @mituharu, #541, fixes #540)
Fix broken coq/saveVo and coq/getDocument requests due to a
parsing problem with extra fields in their requests (@ejgallego,
#547, reported by @Zimmi48)
fcc now understands the --coqlib, --coqcorelib,
--ocamlpath, -Q and -R arguments (@ejgallego, #555)
Describe findlib status in Workspace.describe, which is printed
in the output windows (@ejgallego, #556)
coq-lsp plugin loader will now be strict in case of a plugin
failure, the previous loose behavior was more convenient for the
early releases, but it doesn't make sense now and made things
pretty hard to debug on the Windows installer (@ejgallego, #557)
Add pointers to Windows installers (@ejgallego, #559)
Recognize Goal and Definition $id : ... . as proof starters
(@ejgallego, #561, reported by @Zimmi48, fixes #548)
Provide basic notation information on hover. This is intended for
people to build their own more refined notation feedback systems
(@ejgallego, #562)
Hover request can now be extended by plugins (@ejgallego, #562)
Updated LSP and JS client libs, notably to vscode-languageclient 9
(@ejgallego, #565)
Implement a LIFO document scheduler, this is heavier in the
background as more documents will be checked, but provides a few
usability improvements (@ejgallego, #566, fixes #563, reported by
Ali Caglayan)
New lexical qed detection error recovery rule; this makes a very
large usability difference in practice when editing inside proofs.
(@ejgallego, #567, fixes #33)
coq-lsp is now supported by the coq-nix-toolbox (@Zimmi48,
@CohenCyril, #572, via
https://github.com/coq-community/coq-nix-toolbox/pull/164 )
Support for -rifrom in _CoqProject and in command line
(--rifrom). Thanks to Lasse Blaauwbroek for the report.
(@ejgallego, #581, fixes #579)
Export Query Goals API in VSCode client; this way other extensions
can implement their own commands that query Coq goals (@amblafont,
@ejgallego, #576, closes #558)
New pretac field for preprocessing of goals with a tactic using
speculative execution, this is experimental for now (@amblafont,
@ejgallego, #573, helps with #558)
Implement textDocument/selectionRange request, that will return
the range of the Coq sentence underlying the cursor. In VSCode,
this is triggered by the "Expand Selection" command. The
implementation is partial: we only take into account the first
position, and we only return a single range (Coq sentence) without
parents. (@ejgallego, #582)
Be more robust to mixed-separator windows paths in workspace
detection (@ejgallego, #583, fixes #569)
Adjust printing breaks in error and message panels (@ejgallego,
@Alizter, #586, fixes #457 , fixes #458 , fixes #571)

coq-lsp - 0.1.8+8.16

Published by ejgallego 12 months ago

CHANGES:

Update VSCode client dependencies, should bring some performance
improvements to goal pretty printing (@ejgallego, #530)
Update goal display colors for light mode so they are actually
readable now. (@bhaktishh, #539, fixes #532)
Added link to Python coq-lsp client by Pedro Carrot and Nuno
Saavedra (@Nfsaavedra, #536)
Properly concatenate warnings from _CoqProject (@ejgallego,
reported by @mituharu, #541, fixes #540)
Fix broken coq/saveVo and coq/getDocument requests due to a
parsing problem with extra fields in their requests (@ejgallego,
#547, reported by @Zimmi48)
fcc now understands the --coqlib, --coqcorelib,
--ocamlpath, -Q and -R arguments (@ejgallego, #555)
Describe findlib status in Workspace.describe, which is printed
in the output windows (@ejgallego, #556)
coq-lsp plugin loader will now be strict in case of a plugin
failure, the previous loose behavior was more convenient for the
early releases, but it doesn't make sense now and made things
pretty hard to debug on the Windows installer (@ejgallego, #557)
Add pointers to Windows installers (@ejgallego, #559)
Recognize Goal and Definition $id : ... . as proof starters
(@ejgallego, #561, reported by @Zimmi48, fixes #548)
Provide basic notation information on hover. This is intended for
people to build their own more refined notation feedback systems
(@ejgallego, #562)
Hover request can now be extended by plugins (@ejgallego, #562)
Updated LSP and JS client libs, notably to vscode-languageclient 9
(@ejgallego, #565)
Implement a LIFO document scheduler, this is heavier in the
background as more documents will be checked, but provides a few
usability improvements (@ejgallego, #566, fixes #563, reported by
Ali Caglayan)
New lexical qed detection error recovery rule; this makes a very
large usability difference in practice when editing inside proofs.
(@ejgallego, #567, fixes #33)
coq-lsp is now supported by the coq-nix-toolbox (@Zimmi48,
@CohenCyril, #572, via
https://github.com/coq-community/coq-nix-toolbox/pull/164 )
Support for -rifrom in _CoqProject and in command line
(--rifrom). Thanks to Lasse Blaauwbroek for the report.
(@ejgallego, #581, fixes #579)
Export Query Goals API in VSCode client; this way other extensions
can implement their own commands that query Coq goals (@amblafont,
@ejgallego, #576, closes #558)
New pretac field for preprocessing of goals with a tactic using
speculative execution, this is experimental for now (@amblafont,
@ejgallego, #573, helps with #558)
Implement textDocument/selectionRange request, that will return
the range of the Coq sentence underlying the cursor. In VSCode,
this is triggered by the "Expand Selection" command. The
implementation is partial: we only take into account the first
position, and we only return a single range (Coq sentence) without
parents. (@ejgallego, #582)
Be more robust to mixed-separator windows paths in workspace
detection (@ejgallego, #583, fixes #569)
Adjust printing breaks in error and message panels (@ejgallego,
@Alizter, #586, fixes #457 , fixes #458 , fixes #571)

coq-lsp - 0.1.8+8.17

Published by ejgallego 12 months ago

CHANGES:

Update VSCode client dependencies, should bring some performance
improvements to goal pretty printing (@ejgallego, #530)
Update goal display colors for light mode so they are actually
readable now. (@bhaktishh, #539, fixes #532)
Added link to Python coq-lsp client by Pedro Carrot and Nuno
Saavedra (@Nfsaavedra, #536)
Properly concatenate warnings from _CoqProject (@ejgallego,
reported by @mituharu, #541, fixes #540)
Fix broken coq/saveVo and coq/getDocument requests due to a
parsing problem with extra fields in their requests (@ejgallego,
#547, reported by @Zimmi48)
fcc now understands the --coqlib, --coqcorelib,
--ocamlpath, -Q and -R arguments (@ejgallego, #555)
Describe findlib status in Workspace.describe, which is printed
in the output windows (@ejgallego, #556)
coq-lsp plugin loader will now be strict in case of a plugin
failure, the previous loose behavior was more convenient for the
early releases, but it doesn't make sense now and made things
pretty hard to debug on the Windows installer (@ejgallego, #557)
Add pointers to Windows installers (@ejgallego, #559)
Recognize Goal and Definition $id : ... . as proof starters
(@ejgallego, #561, reported by @Zimmi48, fixes #548)
Provide basic notation information on hover. This is intended for
people to build their own more refined notation feedback systems
(@ejgallego, #562)
Hover request can now be extended by plugins (@ejgallego, #562)
Updated LSP and JS client libs, notably to vscode-languageclient 9
(@ejgallego, #565)
Implement a LIFO document scheduler, this is heavier in the
background as more documents will be checked, but provides a few
usability improvements (@ejgallego, #566, fixes #563, reported by
Ali Caglayan)
New lexical qed detection error recovery rule; this makes a very
large usability difference in practice when editing inside proofs.
(@ejgallego, #567, fixes #33)
coq-lsp is now supported by the coq-nix-toolbox (@Zimmi48,
@CohenCyril, #572, via
https://github.com/coq-community/coq-nix-toolbox/pull/164 )
Support for -rifrom in _CoqProject and in command line
(--rifrom). Thanks to Lasse Blaauwbroek for the report.
(@ejgallego, #581, fixes #579)
Export Query Goals API in VSCode client; this way other extensions
can implement their own commands that query Coq goals (@amblafont,
@ejgallego, #576, closes #558)
New pretac field for preprocessing of goals with a tactic using
speculative execution, this is experimental for now (@amblafont,
@ejgallego, #573, helps with #558)
Implement textDocument/selectionRange request, that will return
the range of the Coq sentence underlying the cursor. In VSCode,
this is triggered by the "Expand Selection" command. The
implementation is partial: we only take into account the first
position, and we only return a single range (Coq sentence) without
parents. (@ejgallego, #582)
Be more robust to mixed-separator windows paths in workspace
detection (@ejgallego, #583, fixes #569)
Adjust printing breaks in error and message panels (@ejgallego,
@Alizter, #586, fixes #457 , fixes #458 , fixes #571)

coq-lsp - 0.1.8+8.18

Published by ejgallego 12 months ago

CHANGES:

Update VSCode client dependencies, should bring some performance
improvements to goal pretty printing (@ejgallego, #530)
Update goal display colors for light mode so they are actually
readable now. (@bhaktishh, #539, fixes #532)
Added link to Python coq-lsp client by Pedro Carrot and Nuno
Saavedra (@Nfsaavedra, #536)
Properly concatenate warnings from _CoqProject (@ejgallego,
reported by @mituharu, #541, fixes #540)
Fix broken coq/saveVo and coq/getDocument requests due to a
parsing problem with extra fields in their requests (@ejgallego,
#547, reported by @Zimmi48)
fcc now understands the --coqlib, --coqcorelib,
--ocamlpath, -Q and -R arguments (@ejgallego, #555)
Describe findlib status in Workspace.describe, which is printed
in the output windows (@ejgallego, #556)
coq-lsp plugin loader will now be strict in case of a plugin
failure, the previous loose behavior was more convenient for the
early releases, but it doesn't make sense now and made things
pretty hard to debug on the Windows installer (@ejgallego, #557)
Add pointers to Windows installers (@ejgallego, #559)
Recognize Goal and Definition $id : ... . as proof starters
(@ejgallego, #561, reported by @Zimmi48, fixes #548)
Provide basic notation information on hover. This is intended for
people to build their own more refined notation feedback systems
(@ejgallego, #562)
Hover request can now be extended by plugins (@ejgallego, #562)
Updated LSP and JS client libs, notably to vscode-languageclient 9
(@ejgallego, #565)
Implement a LIFO document scheduler, this is heavier in the
background as more documents will be checked, but provides a few
usability improvements (@ejgallego, #566, fixes #563, reported by
Ali Caglayan)
New lexical qed detection error recovery rule; this makes a very
large usability difference in practice when editing inside proofs.
(@ejgallego, #567, fixes #33)
coq-lsp is now supported by the coq-nix-toolbox (@Zimmi48,
@CohenCyril, #572, via
https://github.com/coq-community/coq-nix-toolbox/pull/164 )
Support for -rifrom in _CoqProject and in command line
(--rifrom). Thanks to Lasse Blaauwbroek for the report.
(@ejgallego, #581, fixes #579)
Export Query Goals API in VSCode client; this way other extensions
can implement their own commands that query Coq goals (@amblafont,
@ejgallego, #576, closes #558)
New pretac field for preprocessing of goals with a tactic using
speculative execution, this is experimental for now (@amblafont,
@ejgallego, #573, helps with #558)
Implement textDocument/selectionRange request, that will return
the range of the Coq sentence underlying the cursor. In VSCode,
this is triggered by the "Expand Selection" command. The
implementation is partial: we only take into account the first
position, and we only return a single range (Coq sentence) without
parents. (@ejgallego, #582)
Be more robust to mixed-separator windows paths in workspace
detection (@ejgallego, #583, fixes #569)
Adjust printing breaks in error and message panels (@ejgallego,
@Alizter, #586, fixes #457 , fixes #458 , fixes #571)

coq-lsp - 0.1.7+8.18

Published by ejgallego about 1 year ago

CHANGES:

New command line compiler fcc. fcc allows to access most
features of coq-lsp without the need for a command line client,
and it has been designed to be extensible and machine-friendly
(@ejgallego, #507, fixes #472)
Enable web extension support. For now this will not try to start
the coq-lsp worker as it is not yet built. (@ejgallego, #430, fixes
#234)
Improvements and clenaups on hover display, in particular we don't
print repeated Notation strings (@ejgallego, #422)
Don't fail on missing serlib plugins, they are indeed an
optimization; this mostly impacts 8.16 by lowering the SerAPI
requirements (@ejgallego, #421)
Fix bug that prevented "Goal after tactic" from working properly
(@ejgallego, #438, reported by David Ilcinkas)
Fix "Error message browser becomes non-visible when there are many
goals" by using a fixed-position separated error display (@TDiazT,
#445, fixes #441)
Message about workspace detection was printing the wrong file,
(@ejgallego, #444, reported by Alex Sanchez-Stern)
Display the list of pending obligations in info panel (@ejgallego,
#262)
Preliminary support to display document performance data in panel
(@ejgallego, #181)
Fix cases when workspace / root URIs are null, as per LSP spec,
(#453 , reported by orilahav, fixes #283)
Pass implicit argument information to hover printer (@ejgallego, #453,
fixes #448)
Fix keybinding for the "Show Goals at Point" command (@4ever2, #460)
Alert when rootPath is relative (#465, @ejgallego, report by Alex
Sanchez-Stern)
Hook coq-lsp to ViZX extension (@bhaktishh, #469)
proof/goals request now takes an optional formatting parameter
so clients can specify it per-request (@ejgallego, @bhaktishh, #470)
New command line argument --idle-delay=$secs that controls how
much an idle server will sleep before going back to request
processing. Default setting is 0.1, using more aggressive
settings like 0.01 can decrease latency of requests by ~4x
(@ejgallego, @hazardouspeach, #467, #471)
Warnings from _CoqProject files are now applied (@ejgallego,
reported by @arthuraa, #500)
Be more resilient when serializing unknowns Asts (@ejgallego, #503,
reported by Gijs Pennings)
Coq's STM is not linked anymore to coq-lsp (@ejgallego, #511)
More granular options send_perf_data send_diags, verbosity
will set them now (@ejgallego, #517)
Preliminary plugin API for completion events (@ejgallego, #518,
fixes #506)
Limit the number of messages displayed in the goal window to 101,
as to workaround slow render of Coq's pretty printing format. This
is an issue for example in Search where we can get thousand of
results. We also speed up the rendering a bit by not hashing twice,
and fix a parameter-passing bug. (@ejgallego, #523, reported by
Anton Podkopaev)

coq-lsp - 0.1.7+8.16