The Coq mailing list

[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.