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

Document outline doesn't work with on-demand checking #816

Open
Alizter opened this issue Sep 1, 2024 · 1 comment
Open

Document outline doesn't work with on-demand checking #816

Alizter opened this issue Sep 1, 2024 · 1 comment
Labels
kind: bug Something isn't working

Comments

@Alizter
Copy link
Collaborator

Alizter commented Sep 1, 2024 •
edited
Loading

When we are using on-demand checking, the document outline doesn't work. This means we cannot jump to various things without checking the entire document or switching to continuous.

The solution is to make the document outline either incremental, or batch them to be sent when on-demand "finishes checking" what is in the queue. I think incremental would be better since Coq may hang later in the document and it shouldn't affect the symbols appearing before.
@Alizter Alizter added the kind: bug Something isn't working label Sep 1, 2024
@ejgallego
Copy link
Owner

Indeed, this is a PITA; it is easy to try different approaches tho with the current server tho.

I tried a few myself, like sending the outline if on-demand has finished, but didn't like the experience too much.

I think that vsCode doesn't support streaming of the symbols, etc...

Ideally this could be solved maybe a bit better once we move to OCaml 5.3 as a base, and we have implemented lazy proof checking. We could have the idle thread to check the Coq document in idle mode for example, tho this wouldn't work too well for people not using opaque proofs (HoTT?)

Happy to hear more about ideas here.

@ejgallego ejgallego mentioned this issue Sep 29, 2024
Draft
ejgallego added a commit that referenced this issue Sep 29, 2024
@ejgallego
[fleche] New immediate request serving mode.
349fb95 
In this mode, requests are served with whatever document state we
have.

This is very useful when we are not in continuous mode, and we
don't have a good reference as to what to build, for example in
`documentSymbols` (cc: #816)

The mode actually works pretty well in practice as often language
requests will come after goals requests, so the info that is needed is
at hand.

It could also be tried to set the build target for immediate requests
to the view hint, but we should see some motivation for that.

This commit switches `documentSymbols` to the immediate mode, when in
lazy checking mode.
@ejgallego ejgallego mentioned this issue Sep 29, 2024
Merged
ejgallego added a commit that referenced this issue Sep 29, 2024
@ejgallego
[fleche] New immediate request serving mode.
b9d7777 
In this mode, requests are served with whatever document state we
have.

This is very useful when we are not in continuous mode, and we
don't have a good reference as to what to build, for example in
`documentSymbols` (cc: #816)

The mode actually works pretty well in practice as often language
requests will come after goals requests, so the info that is needed is
at hand.

It could also be tried to set the build target for immediate requests
to the view hint, but we should see some motivation for that.

This commit switches `documentSymbols` to the immediate mode, when in
lazy checking mode.
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
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ejgallego @Alizter