Stream: VsCoq devs & users

Topic: Proof View broken


view this post on Zulip 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.

view this post on Zulip Nicolas Margulies (Jun 11 2021 at 16:16):

After a bit of testing, reverting VSCode to its previous version fixes things.

view this post on Zulip Théo Zimmermann (Jun 11 2021 at 16:23):

There's indeed an open issue about that in the vscoq repo.

view this post on Zulip Matthieu Sozeau (Jun 11 2021 at 17:52):

Maybe I got an auto-update then?

view this post on Zulip Fabian Kunze (Jun 14 2021 at 14:56):

The fix is published and the extension can be updated

view this post on Zulip Enrico Tassi (Jun 14 2021 at 15:02):

I'm testing it right away

view this post on Zulip 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!

view this post on Zulip Enrico Tassi (Jun 14 2021 at 15:11):

It works!!! Thanks!

view this post on Zulip 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

view this post on Zulip Enrico Tassi (Jun 16 2021 at 09:58):

did you update the extension? (and restarted code?)

view this post on Zulip Enrico Tassi (Jun 16 2021 at 09:59):

here it did upgrade silently, but then I had to click "reastart needed"

view this post on Zulip Matthieu Sozeau (Jun 16 2021 at 10:12):

I did the reload indeed

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 12:11):

Still not working for me...

view this post on Zulip 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?

view this post on Zulip Enrico Tassi (Jun 18 2021 at 12:18):

I've 1.57.0 (on linux) and it works

view this post on Zulip Enrico Tassi (Jun 18 2021 at 12:19):

oh, and 8.13

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 12:20):

Ha...
8.13 is fine

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 12:20):

I want master

view this post on Zulip Enrico Tassi (Jun 18 2021 at 12:20):

then I guess the issue is different

view this post on Zulip Enrico Tassi (Jun 18 2021 at 12:20):

I mean, it is not the webview problem fixed in 0.3.5

view this post on Zulip Enrico Tassi (Jun 18 2021 at 12:20):

Bug given we are closing on a release, better to investigate

view this post on Zulip Enrico Tassi (Jun 18 2021 at 12:21):

I'll compile master and see

view this post on Zulip Enrico Tassi (Jun 18 2021 at 12:23):

Oh, I see now the other thread

view this post on Zulip Matthieu Sozeau (Jun 18 2021 at 12:24):

Haha lol, I got bitten


Last updated: Mar 29 2024 at 10:01 UTC