Stream: VsCoq devs & users

Topic: Bug ? Change of tab when compiling


view this post on Zulip Guillaume Dubach (Jan 29 2021 at 09:39):

The following might be a bug, or it might just be me not doing the right thing: it happens that I am working with two tabs open, and when compiling the next line with ALT+arrow in tab 2, VsCoq actually goes back to tab 1 and compiles the next line in tab 1. When this happens, what I usually try is to close tab 1 and try again with only tab 2 open, but then quite often it actually re-opens tab 1 and does the same thing. So I eventually close Vscode and open everything again... Am I misunderstanding the commands or is it something that should be fixed ?

view this post on Zulip Meven Lennon-Bertrand (Jan 29 2021 at 09:49):

I do not have a fix, and I sometimes encounter similar problems. What I can at least suggest is that rather than closing and opening VsCode entirely, you can use the "Reload window" feature (accessible from the palette by using Ctrl + Maj + P then typing reload), which usually fixes this kind of problems for me.

view this post on Zulip Théo Winterhalter (Jan 29 2021 at 10:00):

Yeah, same for me. I think there is an issue on the tracker and it might have been fixed already. Eagerly waiting for the next release. :)

view this post on Zulip Théo Winterhalter (Jan 29 2021 at 10:07):

https://github.com/coq-community/vscoq/issues/82

view this post on Zulip Théo Winterhalter (Jan 29 2021 at 10:07):

Seems related.

view this post on Zulip Paolo Giarrusso (Jan 29 2021 at 15:02):

@Théo Winterhalter If that is related, https://github.com/coq-community/vscoq/pull/195 could help.

view this post on Zulip Paolo Giarrusso (Jan 29 2021 at 15:03):

In fact, #195 disables altogether the "feature" that #82 requested: switch to proofview for T when stepping through T.

view this post on Zulip Paolo Giarrusso (Jan 29 2021 at 15:04):

The reason I submitted the revert is that this "feature" is far too aggressive, and switches the proof-view even if you just click (or have the cursor!) in a file.

view this post on Zulip Paolo Giarrusso (Jan 29 2021 at 15:05):

(OTOH, #82 and #195 shouldn't overlap with this bug? Unsure.)

view this post on Zulip Théo Winterhalter (Jan 29 2021 at 15:05):

Yes I saw. I don't know if that helps with @Guillaume Dubach's problem however.


Last updated: Jan 30 2023 at 17:03 UTC