Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Error message browser becomes non-visible when there are many goals. #441

Closed
ejgallego opened this issue Mar 1, 2023 · 4 comments · Fixed by ocaml/opam-repository#24080, ocaml/opam-repository#24081 or ocaml/opam-repository#24440
Closed

Error message browser becomes non-visible when there are many goals. #441

ejgallego opened this issue Mar 1, 2023 · 4 comments · Fixed by ocaml/opam-repository#24080, ocaml/opam-repository#24081 or ocaml/opam-repository#24440
Labels
kind: bug Something isn't working part: goals and info panel
Milestone
0.1.7

Comments

@ejgallego
Copy link
Owner

Reported by Tomás Díaz
@ejgallego ejgallego added the kind: bug Something isn't working label Mar 1, 2023
@ejgallego ejgallego added this to the 0.1.7 milestone Mar 1, 2023
@Alizter
Copy link
Collaborator

Alizter commented Mar 1, 2023

Does it not have a scroll bar?

@ejgallego
Copy link
Owner Author

Yes but the user needs to scroll to see the error.

@Alizter
Copy link
Collaborator

Alizter commented Mar 1, 2023

OK, then in this case it is not really bug but a quality of life improvement. As we discussed before, we should have a divider.

@TDiazT TDiazT mentioned this issue Mar 7, 2023
Merged
ejgallego added a commit that referenced this issue Mar 29, 2023
@ejgallego
Merge pull request #455 from ejgallego/441-error-msg
446707f 
[code] ui: Add divider between errors and goals (#441)
@ejgallego ejgallego modified the milestones: 0.1.7, 0.1.8 Jun 23, 2023
@ejgallego
Copy link
Owner Author

This was fixed by #455 IMO

@ejgallego ejgallego modified the milestones: 0.1.8, 0.1.7 Jul 7, 2023
@ejgallego ejgallego mentioned this issue Jul 7, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jul 7, 2023
@ejgallego
[new release] coq-lsp (0.1.7+8.17)
888aa34 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.16)
20f9c62 
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 ejgallego mentioned this issue Jul 7, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Jul 7, 2023
@ejgallego
[new release] coq-lsp (0.1.7+8.16)
989b30c 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.17)
d8e97f2 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.17)
d1c2e65 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.16)
dd56fb9 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.16)
f6a8427 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.17)
b438d69 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.18)
96fb7c7 
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 ejgallego mentioned this issue Sep 14, 2023
Merged
ejgallego added a commit to ejgallego/opam-repository that referenced this issue Sep 16, 2023
@ejgallego
[new release] coq-lsp (0.1.7+8.18)
3ee21d3 
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
@ejgallego
[new release] coq-lsp (0.1.7+8.18)
26d2b05 
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
@ejgallego @nberth
[new release] coq-lsp (0.1.7+8.17)
14cfb15 
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
@ejgallego @nberth
[new release] coq-lsp (0.1.7+8.16)
f7186b5 
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
@ejgallego @nberth
[new release] coq-lsp (0.1.7+8.18)
89cf154 
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
Assignees
No one assigned
Labels
kind: bug Something isn't working part: goals and info panel
Projects
None yet
Milestone
0.1.7
2 participants
@ejgallego @Alizter