feat: completions for vernac commands

[shilangyu]

out.mp4

This PR implements LSP completions for vernac commands. Please see the README in language-server/dm/indices for a short explanation how this was achieved. Next, I want to implement completions for:

1. Options/Flags (a bit harder, we need to first check that the vernac starts with Set/Unset/Test etc)
2. Attributes (harder, these can be added only in specific places)
3. Tactics (harder, we need to make sure we are in Ltac1 proof mode)

These PRs are targeting builtins, ie those for which completion support has to be hardcoded. I would appreciate input from someone that works on Rocq to tell me if my indices generator (see the mentioned README) has some path to be merged into Rocq.

These indices could be also used to provide on-hover documentation for all builtins.

[shilangyu]

I know there is a large refactor going on in #1046, I am happy to rebase once that is merged.

[SkySkimmer]

the grammar can be gotten from the runtime (cf Print Grammar) but is disconnected from documentation and would need some processing to be used for completion

[shilangyu]

Would you recommend some implementation path that uses Print Grammar and connects it to the documentation?

[shilangyu]

Would be nice to have a way that works with plugins that define their own vernac too

[SkySkimmer]

IDK how feasible it would be to connect it with the doc

[jfehrle]

The grammar described in the documentation is an edited version of the parser's grammar. Print Grammar gives you the parser's grammar. The version in the doc is edited for readability. At build time, the doc_grammar tool generates a grammar file orderedGrammar that covers the built-in commands. That is another way to get the data for command completion. This is described in doc/tools/docgram/README.md. The file includes Rocq-defined plugins. It doesn't include Ltac1- and Ltac2-defined tactics, nor does it tell you what Rocq options are available in the Set command.

[gares]

Nice! I think it is mandatory that the generator is merged in the rocq documentation pipeline first. vsrocq should just ask rocq this json file and use it.

Did you open a PR on rocq? I think the discussion should happen there.

[gares]

About the rendering in the popup, it seems it does not use the same style of the rocq manual, I mean the grammar is way less readable in the popup than in the manual. Is this too hard?

[SkySkimmer]

The doc definitely needs postprocessing, eg for extraction https://rocq-prover.org/doc/master/refman/addendum/extraction.html#rocq:cmd.Extraction the doc combines a few syntaxes so the first paragraph reads "The first two forms display the extracted term(s) as a convenient preview: ..." which is impossible to understand when associated to a completion.

[shilangyu]

vsrocq should just ask rocq this json file and use it.

That would mean users could benefit from this feature only starting 9.3 the earliest. That would leave out a large portion of users.

Did you open a PR on rocq? I think the discussion should happen there.

I will open a PR and see what can be done about it in a discussion there.

About the rendering in the popup, it seems it does not use the same style of the rocq manual, I mean the grammar is way less readable in the popup than in the manual. Is this too hard?

Yes, it is rather difficult. The documentation in the popup is best effort and will certainly not give optimal results...

The doc definitely needs postprocessing, eg for extraction rocq-prover.org/doc/master/refman/addendum/extraction.html#rocq:cmd.Extraction the doc combines a few syntaxes so the first paragraph reads "The first two forms display the extracted term(s) as a convenient preview: ..." which is impossible to understand when associated to a completion.

...hence why I link to the official docs for the full description.

As I wrote in the README, making the results better (same goes to snippets which are not always optimally formatted) requires more heuristics. The example with grammar is something that could be improved by being smarter in docs extraction. Similarly, we can extract which tactics/commands/etc are deprecated and send that through the LSP too. Of course, ideally I would be interested in producing a perfect JSON index that would not have snippets/descriptions which feel out of place. I am very open to discussing alternatives.

[gares]

Yes, it is rather difficult. The documentation in the popup is best effort and will certainly not give optimal results...

I'm fine having in the sources of vsrocq the json file for stable rocq versions, your remark makes a lot of sense.

But I also want to tool to generate it to be part of rocq, be maintained there, and the .json to be pushed next to the refman at each release. Then each Rocq release we can download and vendor the latest version.

[gares]

As I wrote in the README, making the results better (same goes to snippets which are not always optimally formatted) requires more heuristics.

Sorry, but I'm very ignorant on what can be done in that popup window. Can we load remote content in a browser like window (i.e. follow the link you give) and if offline (or while downloading) use the best effort extract you use today? Does this make any sense?

[gares]

And for the record, I'm really happy this feature comes to existence, I've always liked the corresponding company-coq feature. If possible, I want to take full advantage of the web tech we have at hand.

[shilangyu]

As I wrote in the README, making the results better (same goes to snippets which are not always optimally formatted) requires more heuristics.

Sorry, but I'm very ignorant on what can be done in that popup window. Can we load remote content in a browser like window (i.e. follow the link you give) and if offline (or while downloading) use the best effort extract you use today? Does this make any sense?

I am afraid this is not really possible. The LSP protocol expects a raw string here (either plain text or markdown). To show the refman docs here we would have to:

1. Download the entire html/css of the page
2. Find which part of the html corresponds to the docs
3. Render the html/css fragment into markdown

Even if someone would do all of that effort I believe the results would be very iffy as well.

And for the record, I'm really happy this feature comes to existence, I've always liked the corresponding company-coq feature

Me too! I looked at how other editors (company-coq/coqide/coqtail/rocqlsp) implement similar completion features, and they either don't, or it is quite hacky. Granted, this solution is rather hacky too, but I firmly believe we can get in vsrocq something that is better and more robust than in other editors.

[jfehrle]

I am afraid this is not really possible. The LSP protocol expects a raw string here (either plain text or markdown). To show the refman docs here we would have to:

1. Download the entire html/css of the page
2. Find which part of the html corresponds to the docs
3. Render the html/css fragment into markdown

Converting HTML to markdown will lose a lot. The formatting will be a mess (a compromise at best). Hyperlinks for grammar nonterminals and command names will break. The code may be fragile and hard to maintain. Also the conversion to markdown seems like it would be completely specific to vsRocq--supporting another IDE would need completely different code. Much better to find a way to properly display a chunk of the documentation HTML. If vs doesn't have full HTML support, then maybe consider whether there's a reasonable way to use interprocess communication so the vsRocq can direct a browser to show the right stuff on demand without the user having to explicitly request to see it. Perhaps you could use a file to communicate and a bit of Javascript in the browser to poll the file.

For # 2, each command, tactic, etc. has a hyperlink defined that points to the start of the relevant text. Surely the LSP protocol could return that hyperlink instead of the HTML.

There should be a way to enable autocomplete and showing the doc separately.

[shilangyu]

Converting HTML to markdown will lose a lot. The formatting will be a mess (a compromise at best).

I agree. And hence I would really like to avoid this if possible. Currently, I transform Sphinx doctrees which are essentially an AST for document formats. Producing markdown (or plain text like I do currently) from that is less hacky.

Also the conversion to markdown seems like it would be completely specific to vsRocq--supporting another IDE would need completely different code.

I don't believe this is true. A large part of VSRocq is the implementation of an LSP. The purpose is that it is editor agnostic (as long as the editor implements an LSP driver, which many editors do (Neovim, emacs, Zed, Intellij, etc)). In fact, I have a secret agenda of contributing to VSRocq's LSP server to eventually be able to use Rocq in Neovim.

For # 2, each command, tactic, etc. has a hyperlink defined that points to the start of the relevant text. Surely the LSP protocol could return that hyperlink instead of the HTML.

Unless you mean something else, this is what we do currently.

There should be a way to enable autocomplete and showing the doc separately.

I would really like to do that. Do you have some recommendations? For completions we can query Print Grammar, but this is completely disconnected from the docs and I am not sure how we would connect it to them.

[jfehrle]

Currently, I transform Sphinx doctrees which are essentially an AST for document formats.

Even if you generate it from the AST, it looks much worse than the HTML doc. Compare the screen shot in @gares comment above with the rendered HTML:

Enabling autocomplete and doc display seem like they should be controlled in vsRocq but unknown to the Rocq server. They're just booleans. Looks like you already have autocomplete for command names. I was not suggesting going beyond that, just having a way for users to turn what you do have on and off.

However, it feels like we're not really in sync and would be tedious to write it all out in comments here. Let me know if you want to do a video call (I am in California). We can exchange views, but I'm only offering ideas and suggestions--it's your choice whether to adopt them.

[shilangyu]

@jfehrle next week there will be a Rocq call on this topic: https://rocq-prover.zulipchat.com/#narrow/channel/237656-Rocq-devs-.26-plugin-devs/topic/rocq.20call

You are welcome to join.