Stream: Coq users

Topic: Qed. doesn't finish


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

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

view this post on Zulip 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: Jan 27 2023 at 00:03 UTC