Michael Soegtrop (Mar 11 2022 at 09:01): 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.
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 *.
Michael Soegtrop (Mar 11 2022 at 10:37):I am also using -, the +, then *. It happens on the second level.
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 ".".
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 ...
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.
Notification Bot (Mar 11 2022 at 12:49):Michael Soegtrop has marked this topic as resolved.
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
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 :-|
Maxime Dénès (Mar 11 2022 at 15:35):It's a shame Coq is not recognized as an Olympic sport :)
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).
Paolo Giarrusso (Mar 11 2022 at 19:30):What's the Coq shortcut? "Coq: Reset" only works sometimes
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: Oct 13 2024 at 01:02 UTC