multiple webviews · VsCoq devs & users

ok so after a private message conversation I found out that VsCoq opens a webview for every coq file! and this causes weird UX, for example when the user switches to another file the webview for that file is not automatically focused. and some webviews are just buried away. after some sleuthing I found that we managed to automatically focus the webview, then we broke that feature again, and again. I have a hunch that this is not sustainable. is it a good idea for us to use a single webview for the whole editor? and am I missing something?

bubble sort now (deactivated) (Dec 22 2022 at 16:50):

like our Laurent Théry found out this issue in the #VsCoq devs & users > Release 0.3.7 thread. I was like really surprised, but then I realized this is not my fault at all since the majority of my changes are in the webview files, not other code. and if this issue is already persistent then I guess it's time to find a resolution that works

Paolo Giarrusso (Dec 22 2022 at 16:57):

is it a good idea for us to use a single webview for the whole editor?

that would prevent looking at multiple goals in parallel

Paolo Giarrusso (Dec 22 2022 at 17:01):

I totally agree today's experience is annoying; but we had a "fix" at some point — https://github.com/coq-community/vscoq/pull/143 — but it
was overeager so I submitted a revert: https://github.com/coq-community/vscoq/pull/195 — it would open the proof view even when not stepping

bubble sort now (deactivated) (Dec 22 2022 at 17:14):

actually I have a solution for the looking at goals in parallel. we can open multiple vscode windows! this is much less annoying, isn't it. so exactly 1 webview for each vscode window would be reasonable

bubble sort now (deactivated) (Dec 22 2022 at 17:19):

this is Lean's behavior IIRC, and Lean is generally praised for good editor UX

bubble sort now (deactivated) (Dec 22 2022 at 17:25):

maybe allow me some time to think. I might come up with a more reasonable solution

Paolo Giarrusso (Dec 22 2022 at 18:24):

today I can't open two vscode windows on the same folder, so it seems odd — even if you can force it safely, the GUI wouldn't expect that

Paolo Giarrusso (Dec 22 2022 at 18:26):

and one point of editing two files is to look at the proof state from B when updating the needed theory in A (where B depends on A). Where the same goal in B might need multiple A

Paolo Giarrusso (Dec 22 2022 at 18:30):

"at work" my average VScode window has 5-10 proof views open; all I'd want is a "show proof view for this buffer" combo. If some want it automatically it's a reasonable option, as long as it can be disabled and it doesn't stop me from reading other files

Paolo Giarrusso (Dec 22 2022 at 18:32):

other use case: I'm doing proofs in B so I must _read_ A, but I still need to step through it to see contexts/inferred types/etc

Paolo Giarrusso (Dec 22 2022 at 18:38):

also, regardless of individual preferences, I suspect we should balance between evolution and "preserving current expectations", both because there's an existing userbase and because we have somewhat limited resources...

OTOH, I'm not a UX specialist so take all this as "my 2 cents"

Emilio Jesús Gallego Arias (Dec 22 2022 at 18:55):

That's a very interesting discussion, in coq-lsp (and jsCoq) we keep a single goal view, because the main command is "show goals at point"

and one point of editing two files is to look at the proof state from B when updating the needed theory in A (where B depends on A). Where the same goal in B might need multiple A

Umm, maybe you would like the goal buffer to have something like "bookmarks" so could quickly switch between views? What would be your ideal UI for this use case

Paolo Giarrusso (Dec 22 2022 at 22:08):

I'm probably having tunnel vision: what you suggest is probably a good default, but I guess it shouldn't be mandatory. Even a single Goals view is probably better than 20 where I can never find the right one so I need support to jump to it... but being able to fork the Goals view seems interesting? and if there's an auto-update, a "freeze" shortcut might be nice?

Paolo Giarrusso (Dec 22 2022 at 22:09):

ah, I guess "freeze" is what you meant by "bookmark" — sorry! I did read, I just didn't understand :sweat_smile:

Emilio Jesús Gallego Arias (Dec 22 2022 at 23:07):

Yes, bookmark is like freeze I guess. I said bookmark because all you need in the UI side is the point in a buffer, then you query for the buffer. You can do that in jsCoq, Ctrl-click will display goals at point.

Indeed the whole goal display setup of PG-like stuff (including vsCoq it seems) is far from good, there is not reason that when the check of a document progress, the goal info is updated. This is just inheritance from the REPL days.

So now we have a query API for Coq that is "I give you this point in the project, here are the goals", how to display and process that is indeed an interesting problem; I'm not so fond of any of the current solutions, but feedback like yours is very important to think about what we can do.

Emilio Jesús Gallego Arias (Dec 22 2022 at 23:08):

I already got a few ideas for the goal buffer indeed.

Emilio Jesús Gallego Arias (Dec 22 2022 at 23:11):

And actually it is very interesting you are talking about "repair" UIs, this is something we've been discussing locally for a while.

Paolo Giarrusso (Dec 23 2022 at 00:31):

Makes all sense. As an extra point: Does the setup you suggest also work when sentences are very slow? I understand there's prior art for it, but the REPL-like think might make more sense in those cases if you're changing the script and want to finish some edit before resuming processing. At least, if you have proper and quick interruption that just wastes CPU cycles but doesn't slow down steps that are "intended"

Maxime Dénès (Dec 23 2022 at 01:31):

Note that in the the VsCoq2 branch that is being built, the goals logic will indeed be that the UI requests goal infos. It will no longer be Coq who decides when to send these updates when checking the document. VsCoq's behavior in this respect is legacy from REPL and CoqIDE/STM times.

bubble sort now (deactivated) (Dec 23 2022 at 02:16):

(deleted)

Paolo Giarrusso (Dec 23 2022 at 06:56):

@Maxime Dénès same question: so how do you get Coq to notify completion of slow sentences, say if a sentence takes 1s/10s/longer? IIUC you're inspired by Isabelle, but I'm not sure how they handle it, or if it was even common

Emilio Jesús Gallego Arias (Dec 24 2022 at 01:38):

Paolo Giarrusso said: