I have a proof where I can step through all the goals, but when I reach Qed, it hangs. I waited for 3 hours, and it was never completed. I checked this issue on both Coq versions 8.17 and 8.18.0. Running Show Proof results in a relatively small output (~180 lines). This appears to be a serious bug. Should I file a report on the GitHub bug tracker? The environment to reproduce it is rather heavy, with many dependencies. My second question is whether there is a possible workaround?

https://github.com/coq/coq/wiki/Troubleshooting#what-can-i-do-when-qed-is-slow

Does slowness correlate with size of proof object? Because my proof object (just before Qed) is very small and quite trivial.

No. Not until your proof object is hundreds or thousands of megabytes in size

Here is mine: https://gist.github.com/vzaliva/a30bfff4d277ace76c5fc94348b773ba

This is output of `Show Proof.`

Just before `Qed.`

That is not the full proof object, you have `...`

. Try `Set Printing Depth 10000000000`

You also want `Set Printing All`

to see all the hidden terms

The correlation with proof object size is dwarfed by the time it takes to run conversion, universe checking, and, occasionally, guard checking. Of these, only guard checking has any sort of meaningful dependency on proof term size, but it's not always monotonic.

(Also, the relevant measure of proof term size is not lines but words)

Ok, with depth it is 35K lines :)

Right. I just giving a quick assessment of the size from my emacs output buffer line count.

Yeah, the proof object you pasted initially is just from the first 9 calls to `destruct`

I was brute-forcing proof of two functions equivalence which had many `match`

statements which indeed caused explosion of brahcnes

but most of them I was automatically proving by finding a contradiction.

I guess there is no easy way to decrease number of destructs

I will leave it overnight to see if it finishes the Qed and will try to see tomorrow morning what could be done to speed things up following the link you sent

thanks!

It might be of more help if you post the proof. I had such issues before and I always found ways around them. The link Jason initially posted is currently the best resource of hints on this I am aware of.

Usually what made Qed slow for me was doing a `change`

in a hypothesis - using replace instead can result in astronomic speed up factors in Qed time. If a few rules are observed, Qed should not take longer than the construction of the proof term.

This topic was moved to #Coq users > Coq hangs on Qed by Karl Palmskog.

Last updated: Oct 13 2024 at 01:02 UTC