Stream: VsCoq devs & users

Topic: ✔ VsCoq won't start second bullet in (rare) cases


view this post on Zulip Michael Soegtrop (Mar 11 2022 at 09:01):

I have a case where I apply a lemma with 4 premises, which generates 4 goals. I use + to start the first goal - fine. But then VsCoq won't let me start the second goal. {} instead of bullets work and in CoqIDE bullets also work. Has someone seen this on a simple case? Mine is a bit intricate and I can't share it anyway, but if nobody has seen this I try to create a reproduction case.

view this post on Zulip Théo Winterhalter (Mar 11 2022 at 09:07):

Do you have the same with - instead of +? I have never seen that but I always do - then + then *.

view this post on Zulip Michael Soegtrop (Mar 11 2022 at 10:37):

I am also using -, the +, then *. It happens on the second level.

view this post on Zulip Fabian Kunze (Mar 11 2022 at 12:26):

Are you using nested proofs, or other "more complicated" scenarios than a list of Definition/lemmas? (maybe involving nesting modules and sections, or using custom notation making use of the symbol ".".

view this post on Zulip Michael Soegtrop (Mar 11 2022 at 12:34):

No, it is a clean proof. Since this doesn't seem to happen frequently I try to boil it down to a repro case ...

view this post on Zulip Michael Soegtrop (Mar 11 2022 at 12:49):

It looks like it was a temporary hick-up. If I close and reload the file it does work - so no way to reproduce it.

view this post on Zulip Notification Bot (Mar 11 2022 at 12:49):

Michael Soegtrop has marked this topic as resolved.

view this post on Zulip Yannick Forster (Mar 11 2022 at 15:11):

I have seen similar hick-ups when I edited the white space between lemmas. So for instance if I remove an empty line, VsCoq will just go on without re-processing anything (which is good), but might get very confused by the missing line afterwards, so only reloading helps

view this post on Zulip Paolo Giarrusso (Mar 11 2022 at 15:21):

yes, it's better now but there's a reason I still have "Reload Window" in muscle memory :-|

view this post on Zulip Maxime Dénès (Mar 11 2022 at 15:35):

It's a shame Coq is not recognized as an Olympic sport :)

view this post on Zulip Enrico Tassi (Mar 11 2022 at 17:23):

We are in good company, I've to restart the ocaml language server every time I play with a module type... they did even add a shortcut to just restart it instead of reloading the window (there is the same for Coq, btw).

view this post on Zulip Paolo Giarrusso (Mar 11 2022 at 19:30):

What's the Coq shortcut? "Coq: Reset" only works sometimes

view this post on Zulip Enrico Tassi (Mar 12 2022 at 06:58):

that one. it does not work in all cases right.
there you restart the extension host, still faster that restarting the window.


Last updated: Jan 30 2023 at 18:04 UTC