Lutz Wrage (Apr 26 2021 at 12:34): Lutz Wrage (Apr 26 2021 at 12:34):I ran into a situation where a proof seems to work fine (no more subgoals) but then Qed seems to run forever. I am fairly new to Coq, so I have no idea how to deal with this. Are there certain situations where this happens, or is this not a common occurrence? Is this some kind of limitation I'm not aware of? Is there some known approach to work around it?
Yannick Forster (Apr 26 2021 at 12:54):There are certain situations where this happens (here's a recent one: https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/How.20to.20Debug.20slow.20QED.3F) but from my experience it is not common. Can you give some more context or even show an excerpt of your file / the whole file?
Michael Soegtrop (Apr 26 2021 at 17:02):What helped me in the end is the OCaml debugger. With an endless Qed it is easy to break in the right spot (just hit Ctrl+C after a minute) and one can go back and forth in time in ocamldebug. The Coq printers produce readable result for the kernel terms involved which where easy to recognize for me although I don't know much about the Coq kernel. If you are on Mac you need a few tweaks to get the printers loaded. Other methods didn't really help me to debug my Qed issue.
In my case the root cause was a hnf in a hypothesis.
Last updated: Oct 04 2023 at 20:01 UTC