Guillaume Dubach (Jan 29 2021 at 09:39): 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 ?
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.
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. :)
Théo Winterhalter (Jan 29 2021 at 10:07):https://github.com/coq-community/vscoq/issues/82
Théo Winterhalter (Jan 29 2021 at 10:07):Seems related.
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.
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.
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.
Paolo Giarrusso (Jan 29 2021 at 15:05):(OTOH, #82 and #195 shouldn't overlap with this bug? Unsure.)
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: Jun 04 2023 at 23:30 UTC