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 ?
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.
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 If that is related, https://github.com/coq-community/vscoq/pull/195 could help.
In fact, #195 disables altogether the "feature" that #82 requested: switch to proofview for T when stepping through T.
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.
(OTOH, #82 and #195 shouldn't overlap with this bug? Unsure.)
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