Enhancement: action to jump to next/previous Coq sentence

[Blaisorblade]

This would improve navigation through the different steps of a proof.

Cursor shortcuts to jump to the previous/next dot are only a poor approximation, since a single tactic can contain multiple dots.

https://coq.zulipchat.com/#narrow/stream/329642-coq-lsp/topic/.22Stepping.22.20in.20continuous.20mode

[Alizter]

Since we have access to the parser we should be able to step to the next vernac/tactic sentence.

For the time being, we shouldn't choose a shortcut for this in VSCode until we think a little harder about it. Ctrl + Right arrow is useful as a shortcut for skipping words on its own already. I say that we add the functionality and let users configure their own keymappings to it.

[Alizter]

I just realised that previous me has also wanted this:

• Shortcut for jump to next sentence #263

[ejgallego]

Indeed let's try to ship this soon.

My only question is if implementing some of these calls would be of help here:

• https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_semanticTokens
• https://microsoft.github.io/language-server-protocol/specifications/lsp/3.17/specification/#textDocument_selectionRange

Could be of help here? Do you folks know what are the commands to skip to next sentence for other languages, like C or Rust?

Also there are two implementation strategies:

• a pure client code: IMHO a regexp should work 99% of the time.
• a server-aided implementation: here the problem is that this can introduce some non-trivial latency, so indeed that's something to take into account.

IMHO in an ideal world, VSCode would take via LSP something like semantic Tokens, which would then just allow VSCo to implement navigation commands. A problem for this is that we'd really need a streaming implementation of the call, which few clients support (VSCode does not).

I think Lean4 is using semantic Tokens already, it'd be good to see if they managed to get that working. Actually I did open some discussion about this in the LSP repos upstream IIRC.

[ejgallego]

Oh, also note, lambdapi VSCode client can do this; we could just use that code, that'd be a quick way to alleviate this for now.

[ejgallego]

Another interesting command is "Go to Next folding Range"

[ejgallego]

And the last option is to use the textmate grammar to approx sentences.

[Alizter]

I don't know of any other language server that has this functionality apart from other proof assistants TBH. In agda emacs you have a go to next hole shortcut and even OCaml has a similar go to hole functionality. Moving the cursor doesn't provide any interaction for most programming languages, its only here that it updates the state of the language server. In nvim for instance, you can see the equivalent of vscodes tooltips by moving the cursor over an error, but there you have vim movement which makes things much easier.

[Alizter]

The idea about semantics tokens sounds interesting but I haven't thought about it before.

[ejgallego]

Indeed, there are many ways to approach this problem!