[client] debug setting #217
Conversation
There was a problem hiding this comment.
I am not sure why we should bother the user with these flags, which are really internal.
Is there a way to hide these options by default?
Already the clutter in the settings panel is not good, so I'm unsure about this, seems like something it will impact all users a lot while the developers will barely benefit.
|
I guess we can expose a single |
|
We don't have to have these settings available in the UI at all. We could just allow users to type the settings directly in their config. There is precedent for this kind of behavior in other extensions. |
If that can be done then it's good. If not we should IMO only expose a generic |
Alizter
force-pushed
the
ps/rr/debug_settings
branch
from
aa9e97d
to
0b39571
Compare
|
@ejgallego This now works, you can configure the debug settings in your settings.json. The UI only shows a small debug entry which tells you to edit from settings.json. I had to change the order in which coq was initialized so it came after recieving the init settings from the config. |
Alizter
force-pushed
the
ps/rr/debug_settings
branch
2 times, most recently
from
215e7f2
to
c0ebe51
Compare
Alizter
added
kind: enhancement
Alizter
force-pushed
the
ps/rr/debug_settings
branch
from
c0ebe51
to
bb0b4b7
Compare
controller/coq_lsp.ml
Outdated
| (* LSP Server server initialization *) | ||
| let workspace = lsp_init_loop ic oc ~cmdline in | ||
|
|
||
| let fb_queue = Coq.Protect.fb_queue in | ||
| let root_state = coq_init ~fb_queue ~bt in |
There was a problem hiding this comment.
The order here has to go back to coq_init first, then workspace init after.
That's not a big deal workspace initialization can take care of the debug stuff.
But indeed backtraces are special, for example you often want them to be enabled before the lsp_init loop takes place.
There was a problem hiding this comment.
If I don't do this then backtraces are not picked up from the settings. What is your suggestion for this?
There was a problem hiding this comment.
Have Workspace.apply set it too, you'll need to add the option to the particular workspace setting.
Alizter
force-pushed
the
ps/rr/debug_settings
branch
from
bb0b4b7
to
17cdb8b
Compare
|
I've gone for a more direct way of setting backtraces. I put it in the loop so if the setting is changed for example after loading the config, it is able to trace. Didn't really understand your Workspace.apply suggestion. I've also removed the useless -bt flag. |
<!-- ps-id: c6aaf75b-0994-4ab7-a173-e9f77c462266 --> Signed-off-by: Ali Caglayan <alizter@gmail.com>
Alizter
force-pushed
the
ps/rr/debug_settings
branch
from
17cdb8b
to
4ad7a1c
Compare
|
Maybe I am not so happy with this in the end. |
Sorry I didn't explain it properly, see #247 |
|
I'd suggest we resurrect this PR, but only exposing a backtraces / debug flag in the vscode side. |
|
@ejgallego Feel free to take over. |
This is a simpler version of #217 Co-authored-by: Ali Caglayan <alizter@gmail.com>
This is a simpler version of #217 Co-authored-by: Ali Caglayan <alizter@gmail.com>
This is a simpler version of #217 Co-authored-by: Ali Caglayan <alizter@gmail.com>
This is a simpler version of #217 Co-authored-by: Ali Caglayan <alizter@gmail.com>
CHANGES: --------------------- - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184) - The keybinding alt+enter in VSCode is now correctly scoped to be only active on Coq files (@artagnon, ejgallego/coq-lsp#188) - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197) - The info view is now script enabled and does client-side rendering. It is also now bundled with esbuild as part of the build process (@artagnon, @ejgallego, ejgallego/coq-lsp#171) - The no-op `--std` argument to the `coq-lsp` binary has been removed, beware of your setup in the extension settings (@ejgallego, ejgallego/coq-lsp#208) - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212) - `GoalAnswer`s now include the proof "stack" and better hypothesis information, changes are compatible with 0.1.3 `GoalAnswer` version (@ejgallego, ejgallego/coq-lsp#237) - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242, fixes ejgallego/coq-lsp#224) - In `_CoqProject`, `-impredicative-set` is now parsed correctly (@artagnon, ejgallego/coq-lsp#241) - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223) - `debug` option in the client / protocol that will enable Coq's backtraces (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248) - Full document stats are now correctly computed on checking resumption, still cached sentences will display the cached timing tho (@ejgallego, ejgallego/coq-lsp#257) - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260) - `_CoqProject` file is now detected using LSP client `rootPath` (@ejgallego, ejgallego/coq-lsp#261) - Press `\` to trigger Unicode completion by the server. This behavior is configurable, with "off", "regular", and extended settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
CHANGES: --------------------- - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184) - The keybinding alt+enter in VSCode is now correctly scoped to be only active on Coq files (@artagnon, ejgallego/coq-lsp#188) - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197) - The info view is now script enabled and does client-side rendering. It is also now bundled with esbuild as part of the build process (@artagnon, @ejgallego, ejgallego/coq-lsp#171) - The no-op `--std` argument to the `coq-lsp` binary has been removed, beware of your setup in the extension settings (@ejgallego, ejgallego/coq-lsp#208) - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212) - `GoalAnswer`s now include the proof "stack" and better hypothesis information, changes are compatible with 0.1.3 `GoalAnswer` version (@ejgallego, ejgallego/coq-lsp#237) - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242, fixes ejgallego/coq-lsp#224) - In `_CoqProject`, `-impredicative-set` is now parsed correctly (@artagnon, ejgallego/coq-lsp#241) - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223) - `debug` option in the client / protocol that will enable Coq's backtraces (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248) - Full document stats are now correctly computed on checking resumption, still cached sentences will display the cached timing tho (@ejgallego, ejgallego/coq-lsp#257) - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260) - `_CoqProject` file is now detected using LSP client `rootPath` (@ejgallego, ejgallego/coq-lsp#261) - You can press `\` to trigger Unicode completion by the server. This behavior is configurable, with "off", "regular", and "extended" settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
CHANGES: --------------------- - Support for OCaml 4.11 (@ejgallego, ejgallego/coq-lsp#184) - The keybinding alt+enter in VSCode is now correctly scoped to be only active on Coq files (@artagnon, ejgallego/coq-lsp#188) - Support Unicode files (@ejgallego, ejgallego/coq-lsp#200, fixes ejgallego/coq-lsp#193, fixes ejgallego/coq-lsp#197) - The info view is now script enabled and does client-side rendering. It is also now bundled with esbuild as part of the build process (@artagnon, @ejgallego, ejgallego/coq-lsp#171) - The no-op `--std` argument to the `coq-lsp` binary has been removed, beware of your setup in the extension settings (@ejgallego, ejgallego/coq-lsp#208) - Settings for the VSCode extension are now categorized (@Alizter, ejgallego/coq-lsp#212) - `GoalAnswer`s now include the proof "stack" and better hypothesis information, changes are compatible with 0.1.3 `GoalAnswer` version (@ejgallego, ejgallego/coq-lsp#237) - Focus is now preserved when the info view pops up (@artagnon, ejgallego/coq-lsp#242, fixes ejgallego/coq-lsp#224) - In `_CoqProject`, `-impredicative-set` is now parsed correctly (@artagnon, ejgallego/coq-lsp#241) - InfoView is not written in React (@ejgallego, ejgallego/coq-lsp#223) - `debug` option in the client / protocol that will enable Coq's backtraces (@Alizter, @ejgallego, ejgallego/coq-lsp#217, ejgallego/coq-lsp#248) - Full document stats are now correctly computed on checking resumption, still cached sentences will display the cached timing tho (@ejgallego, ejgallego/coq-lsp#257) - Set Coq library name correctly (@ejgallego, ejgallego/coq-lsp#260) - `_CoqProject` file is now detected using LSP client `rootPath` (@ejgallego, ejgallego/coq-lsp#261) - You can press `\` to trigger Unicode completion by the server. This behavior is configurable, with "off", "regular", and "extended" settings (@artagnon, @Alizter, ejgallego, ejgallego/coq-lsp#219).
Signed-off-by: Ali Caglayan alizter@gmail.com