Patrick Nicodemus (Oct 30 2022 at 17:31): 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?
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: Sep 23 2023 at 14:01 UTC