The Coq mailing list

[Enrico Tassi <enrico.tassi AT inria.fr>]

On Mon, Feb 02, 2015 at 08:29:04AM +0000, Soegtrop, Michael wrote:
> Dear Coq Users,
> 
> one thing which doesn't look right in CoqIDE 8.5 (Windows) is that the
> checking of trivial proofs with the asynchronous proof mechanism is
> very slow. As it looks any proof takes at least 15s. So a simple file
> with 4 trivial proofs takes more than 1 minute, although coqc can
> check it in a fraction of a second.

Many thanks for reporting.  I need to know a little more about your file
and also I want to ask you to try the following:

1. Click on "Goto End" (down arrow with a bar)
2. Wait until the bottom right corner progress thingy says "Coq is ready"
3. Then click "Fully check the document" (wheels)

While it is true that, especially for small proofs, the overhead of
delegating them to worker processes is visible, I have 2 remarks:

1. once a small proof delegated the first time, Coq records how long it
   took to delegate it.  Next time, if it took less than 1 sec, it will
   be processed eagherly.  Note that if you press the up arrow with a
   bar, Coq is reastarted so it loses its memory.  So this "optimizaton"
   only works if you jump before and after proofs with the other
   buttons.

2. there is a problem with OCaml threads that results in them not
   being woken up when some data is ready in the socket they are reading
   from.  My work around was to never do a fully blocking read, always
   with a timeout, that is now 1 second.  So if you are very unlucky
   you may experience a slow system because of that.  Could you check in
   the task manager if Coq is using CPU or no?  If it is not computing
   then I guess a possible workaround would be to lower the timeout.  I
   can rebuild the beta for you with this parameter changed.  Which
   windows do you use by the way?
   
   Such bug affects also linux but is way harder to reproduce.  I'll
   eventually dig into it.  Or avoid threads completely, but this
   requires doing some cps transformation of my code and I'm not
   eagher to do that.

Best,
-- 
Enrico Tassi