Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] when Coq is thinking hard, what is it thinking about?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] when Coq is thinking hard, what is it thinking about?


chronological Thread 
  • From: Roman Beslik <beroal AT ukr.net>
  • To: coq-club AT inria.fr
  • Subject: Re: [Coq-Club] when Coq is thinking hard, what is it thinking about?
  • Date: Tue, 28 Sep 2010 15:20:22 +0300
  • Disposition-notification-to: Roman Beslik <beroal AT ukr.net>

The only case when I experienced a similar situation, Coq wasted time on its main job, i.e. checking types. Making some lambda-terms opaque ("Qed." instead of "Defined.") speed up a process 10-100 times, but nevetheless delays were noticeable. Maybe the core of Coq needs optimization.

On 26.09.10 10:12, Adam Megacz wrote:
I have a situation where certain [Class] declarations take an
astonishingly long time for Coq to process (several minutes for just a
few lines on a high-end machine).  Sadly I have not been able to isolate
the problem well enough to submit a concise bug report; I can't figure
out how to trigger the problem with anything less than several hundred
lines of script.

I was hoping that the situation might improve with Coq 8.3, but based on
the limited portions of my development that I've been able to get
working under 8.3 this particular issue actually appears to have gotten
worse.  Moreover, with 8.3 I see much greater memory consumption
(approaching 1GB) when this problem is encountered (under 8.2 memory
consumption was pretty stable).

Is there any way to get Coq to tell me what it's thinking so hard about?

Right now it just sits there silently for a long, long time at 100% CPU
utilization.  I wish I knew what it was doing... I might even be able to
simplify whatever task it's having such trouble with.

So far I've tried "-verbose" and "Typeclasses eauto := debug".  Neither
seems to give helpful information here; they print what you'd expect to
see and then there's no output while Coq goes off and furiously burns
CPU cycles.

I dug around in the development documentation and found out about
#trace, but that seems to be meant for when you know which Ocaml
function you suspect is the culprit.

I'm sort of hoping for a general transcript of what's going on so I can
start narrowing things down and find a workaround of some sort.

Thanks,

   - a







--
Best regards,
  Roman Beslik.




Archive powered by MhonArc 2.6.16.

Top of Page