feature request: Hover should show implicit arguments #448
Labels
Milestone
Comments
|
Yes! Also when hovering on an application we should display the implicits there, however that requires some UI design before implementation. |
|
@Alizter is there a command in Coq that will print types like this? |
|
|
ejgallego
added a commit
that referenced
this issue
Mar 7, 2023
This follows what Coq's `About` does upstream. Note that still the printing is not very satisfactory in some cases, but in this case it seems Coq's `About` has the same problem. So I'd suggest to close #448 and open an issue upstream about general implicit argument printing, WDYT @Alizter ? Fixes #448.
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Jul 7, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Sep 14, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Sep 16, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
ejgallego
added a commit
to ejgallego/opam-repository
that referenced
this issue
Sep 17, 2023
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
nberth
pushed a commit
to nberth/opam-repository
that referenced
this issue
Jun 18, 2024
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, ejgallego/coq-lsp#507, fixes ejgallego/coq-lsp#472) - Enable web extension support. For now this will not try to start the coq-lsp worker as it is not yet built. (@ejgallego, ejgallego/coq-lsp#430, fixes ejgallego/coq-lsp#234) - Improvements and clenaups on hover display, in particular we don't print repeated `Notation` strings (@ejgallego, ejgallego/coq-lsp#422) - Don't fail on missing serlib plugins, they are indeed an optimization; this mostly impacts 8.16 by lowering the SerAPI requirements (@ejgallego, ejgallego/coq-lsp#421) - Fix bug that prevented "Goal after tactic" from working properly (@ejgallego, ejgallego/coq-lsp#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, ejgallego/coq-lsp#445, fixes ejgallego/coq-lsp#441) - Message about workspace detection was printing the wrong file, (@ejgallego, ejgallego/coq-lsp#444, reported by Alex Sanchez-Stern) - Display the list of pending obligations in info panel (@ejgallego, ejgallego/coq-lsp#262) - Preliminary support to display document performance data in panel (@ejgallego, ejgallego/coq-lsp#181) - Fix cases when workspace / root URIs are `null`, as per LSP spec, (ejgallego/coq-lsp#453 , reported by orilahav, fixes ejgallego/coq-lsp#283) - Pass implicit argument information to hover printer (@ejgallego, ejgallego/coq-lsp#453, fixes ejgallego/coq-lsp#448) - Fix keybinding for the "Show Goals at Point" command (@4ever2, ejgallego/coq-lsp#460) - Alert when `rootPath` is relative (ejgallego/coq-lsp#465, @ejgallego, report by Alex Sanchez-Stern) - Hook coq-lsp to ViZX extension (@bhaktishh, ejgallego/coq-lsp#469) - `proof/goals` request now takes an optional formatting parameter so clients can specify it per-request (@ejgallego, @bhaktishh, ejgallego/coq-lsp#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, ejgallego/coq-lsp#467, ejgallego/coq-lsp#471) - Warnings from `_CoqProject` files are now applied (@ejgallego, reported by @arthuraa, ejgallego/coq-lsp#500) - Be more resilient when serializing unknowns Asts (@ejgallego, ejgallego/coq-lsp#503, reported by Gijs Pennings) - Coq's STM is not linked anymore to `coq-lsp` (@ejgallego, ejgallego/coq-lsp#511) - More granular options `send_perf_data` `send_diags`, `verbosity` will set them now (@ejgallego, ejgallego/coq-lsp#517) - Preliminary plugin API for completion events (@ejgallego, ejgallego/coq-lsp#518, fixes ejgallego/coq-lsp#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, ejgallego/coq-lsp#523, reported by Anton Podkopaev)
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
When hovering over a term, all the arguments are currently printed. We should make it so that implicit arguments are printed with
{ }so that they can easily be ignored by the user. I believe not printing them at all is also an option, but may be confusing.The text was updated successfully, but these errors were encountered: