search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
152 stars 32 forks source link

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

Open Alizter opened 2 months ago

Alizter commented 2 months ago

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.

ejgallego commented 2 months ago

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.