coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Slow QED

From: Kenneth Roe <kendroe AT hotmail.com>
To: Coq-Club <coq-club AT inria.fr>
Subject: [Coq-Club] Slow QED
Date: Mon, 22 Apr 2013 11:50:27 -0700
Importance: Normal

I have a proof of about 100 lines. The proof itself takes a few minutes to process in Coq. However, it seems to hang on processing the QED at the end. I waited several hours and it had not completed. The proof involves frequent uses of "compute" to cause some fairly complex function evaluation. Has anyone run into this problem? I can email code to anyone who is interested in looking into the issue.

- Ken

[Coq-Club] Slow QED, Kenneth Roe, 04/22/2013
- Re: [Coq-Club] Slow QED, Thomas Braibant, 04/22/2013
  - RE: [Coq-Club] Slow QED, Kenneth Roe, 04/22/2013
    - Re: [Coq-Club] Slow QED, AUGER Cédric, 04/22/2013
      - Re: [Coq-Club] Slow QED, Thomas Braibant, 04/22/2013
    - Re: [Coq-Club] Slow QED, Thomas Braibant, 04/22/2013
  - Re: [Coq-Club] Slow QED, Frédéric Besson, 04/23/2013