Nicolas Margulies (Jun 11 2021 at 15:26): Nicolas Margulies (Jun 11 2021 at 15:26):@Matthieu Sozeau
Did it start not working today ? Because I do have a problem : The ProofView tab stopped displaying anything. The language server does run in the background and is correctly stepping through the file, but the Proof View stays silent.
I switched between coqHoTT (coq 8.13) and coq 8.11 and it behaved in the same way.
I assume this to be linked in some way to the VSCode update that dropped today.
Nicolas Margulies (Jun 11 2021 at 16:16):After a bit of testing, reverting VSCode to its previous version fixes things.
Théo Zimmermann (Jun 11 2021 at 16:23):There's indeed an open issue about that in the vscoq repo.
Matthieu Sozeau (Jun 11 2021 at 17:52):Maybe I got an auto-update then?
Fabian Kunze (Jun 14 2021 at 14:56):The fix is published and the extension can be updated
Enrico Tassi (Jun 14 2021 at 15:02):I'm testing it right away
Enzo Crance (Jun 14 2021 at 15:04):The proof view was missing too, but after updating it is back on my machine. Thanks for fixing the bug!
Enrico Tassi (Jun 14 2021 at 15:11):It works!!! Thanks!
Matthieu Sozeau (Jun 16 2021 at 09:55):Is the fix in 0.3.5 ? I still have the problem that the proofview does not get updated
Enrico Tassi (Jun 16 2021 at 09:58):did you update the extension? (and restarted code?)
Enrico Tassi (Jun 16 2021 at 09:59):here it did upgrade silently, but then I had to click "reastart needed"
Matthieu Sozeau (Jun 16 2021 at 10:12):I did the reload indeed
Matthieu Sozeau (Jun 18 2021 at 12:11):Still not working for me...
Matthieu Sozeau (Jun 18 2021 at 12:18):Did anyone try on Mac OS with Code version 1.57.1 and VSCoq 0.3.5 and Coq's current master?
Enrico Tassi (Jun 18 2021 at 12:18):I've 1.57.0 (on linux) and it works
Enrico Tassi (Jun 18 2021 at 12:19):oh, and 8.13
Matthieu Sozeau (Jun 18 2021 at 12:20):Ha...
8.13 is fine
Matthieu Sozeau (Jun 18 2021 at 12:20):I want master
Enrico Tassi (Jun 18 2021 at 12:20):then I guess the issue is different
Enrico Tassi (Jun 18 2021 at 12:20):I mean, it is not the webview problem fixed in 0.3.5
Enrico Tassi (Jun 18 2021 at 12:20):Bug given we are closing on a release, better to investigate
Enrico Tassi (Jun 18 2021 at 12:21):I'll compile master and see
Enrico Tassi (Jun 18 2021 at 12:23):Oh, I see now the other thread
Matthieu Sozeau (Jun 18 2021 at 12:24):Haha lol, I got bitten
Last updated: Jun 04 2023 at 22:30 UTC