The Coq mailing list

["Soegtrop, Michael" <michael.soegtrop AT intel.com>]

Dear Enrico,

Indeed, if I do a second check it is quite fast (<1" for a file which first 
time takes 1'40"). Btw.: Even if I press the "up arrow with bar" it is very 
fast when I press "down arrow with bar" a second time.

I will send you a simple sample file via private email. It is really trivial, 
but it takes 1'40" on my machine, which is reasonably fast.

Regarding the reads from the socket: I found this article on stackoverflow: 
http://stackoverflow.com/questions/16729842/socket-onread-onready-onclose-event-handler-function-in-ocaml/16733064.
 At least for Unix there seems to be a solution. Not sure if the same APIs 
are available on Windows. If not, I might be able to find a way.

In case you can set a socket to blocking / non blocking but have no select 
function, one trick which did work for me in the past (not Ocaml, but another 
system where I had similar problems) was to read read just one byte in 
blocking mode and then do a non blocking read for a larger size.
 
Best regards,

Michael

-----Original Message-----
From: 
coq-club-request AT inria.fr
 
[mailto:coq-club-request AT inria.fr]
 On Behalf Of Enrico Tassi
Sent: Monday, February 02, 2015 10:36 AM
To: 
coq-club AT inria.fr
Subject: Re: [Coq-Club] CoqIDE 8.5: asynchronous check of trivial proofs slow 
(always >15s)

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