Stream: Coq users

Topic: Debug long Qed or Defined


view this post on Zulip Patrick Nicodemus (Oct 30 2022 at 17:31):

Sometimes when you end a proof it takes Coq a long time to process the tactic script and actually create the term. How does one debug this when it takes a very long time for Qed or Defined to execute?
Similarly in Program mode it can sometimes take Program a very long time to process the Next Obligation command, does anyone have a suggestion for how I might track down why it is so time consuming?

view this post on Zulip Michael Soegtrop (Oct 31 2022 at 08:51):

There are several longer discussions on this here, e.g. (https://coq.zulipchat.com/#narrow/stream/237977-Coq-users/topic/How.20to.20Debug.20slow.20QED.3F)


Last updated: Feb 08 2023 at 23:03 UTC