Feature request: showing the next bullet

[toku-sa-n]

Hi. I'm using VsCoq, and it's pretty nice! However, I think it'd be great if VsCoq prints the next bullet on the completion of proof for a bullet.

Currently, VsCoq only says "No more subgoals".

Coqtail, a Vim plugin for Coq, has the feature like this.

I'm using VsCoq 2.0.1 and vscoq-language-server 2.0.1+coq8.18.

[SkySkimmer]

You probably want something like https://github.com/coq/coq/blob/a37a2e4bf622d7c2a6a0ec9fe9d58d981a142442/printing/printer.ml#L966-L972
The Proof_bullet.suggest says "focus next goal with bullet -"
pr_subgoals on bgoals = Proof.background_subgoals p does the actual goal printing

[gares]

Thanks @SkySkimmer . If we add a quickfix for that in Coq, there is nothing to do here in VSCoq.

[SkySkimmer]

WDYM? Coq already prints this info (with coqtop in proof general)

[gares]

I mean generating a proper quickfix as in LSP. Warnings as errors can carry one, maybe plain errors cannot yet.I don't recall the API.

I guess the only sensitive piece of info is the loc, I.e. the piece of text to be replaced by the right bullet. If it is a bad bullet, then it is the loc of the whole bullet. If it is a missing bullet, it must be some white space before the tactic.

[SkySkimmer]

There is no warning or error involved here.

[gares]

My guess is that no matter what you write after, you get an error saying that you need a bullet or that the bullet you write is wrong. That is the error we can suggest a fix for.

Maybe it is too convoluted to be usable, I would need to try.

Using the same api for code completion can work as well of course.

[TheoWinterhalter]

I think it should just replace the text that says "No more goals" which is incorrect and replace it with the one Coq outputs.

[rtetley]

I suppose we can do both ?

• Write "There are unfocused goals, focus with blablabla" right after a bullet is solved
• Add a quickfix suggesting a fix if a user writes anything else after ?

[rtetley]

Thanks to @SkySkimmer I now detect unfocused goal (see linked PR).
However all I do is write a message.
Seeing as we already have Shelved and Given Up tabs, would it not make sense to make a Unfocused tab ?
Or should I just display the unfocused goals like Coqtail does ?

[Durbatuluk1701]

Thanks to @SkySkimmer I now detect unfocused goal (see linked PR). However all I do is write a message. Seeing as we already have Shelved and Given Up tabs, would it not make sense to make a Unfocused tab ? Or should I just display the unfocused goals like Coqtail does ?

I would advocate for automatically displaying the unfocused goals (or at the very least making an option to do so). If I have to mouse over to an Unfocused tab to see them I would likely just never do so.

[rtetley]

Okay so I came up with this:

It displays all the unfocused goals but makes them all collapsed by default. WDYT ?

[TheoWinterhalter]

Shouldn't it say "focus with bullet"?

[rtetley]

Good catch 😅