Thanks David. I'll try the CVS version of poly.
Is there anyway GC could be deferred, or interrupted, during an interactive session?
Tom
2008/5/28 David Matthews David.Matthews@prolingua.co.uk:
Dear Tom, Your example is essentially doing nothing but growing the stack. The stack is held in the heap and whenever the current segment runs out a new, larger, segment is allocated and the current contents of the stack are copied into that. That can result in garbage collection.
Both garbage collection and stack copying are non-interruptible so in either case an interrupt will be deferred until the action is complete. The handling of ctrl/C has been improved in the CVS version compared with the 5.1 release but there are still delays if ctrl/C is pressed during a garbage collection.
While investigating this I did discover a bug that resulted in the garbage collector saying that there was insufficient space to extend the stack when in fact there was enough. It's likely now that your example would result in a Warning - Stack limit reached - interrupting process message since the stack will probably run out before the ctrl/C is processed.
There may be more of a problem with the 64-bit version than the 32-bit version because the maximum size of a stack segment is larger in the 64-bit version so the limitation is likely to be the overall memory rather than the stack size.
David
Tom Ridge wrote:
Dear David,
I just tried the following experiment in poly (see below).
Under mosml, ctrl-c causes an almost instantaneous return to top-level. Under poly, the time to return seems dependent on the depth of recursion(!). Does this sound possible? Is there anyway to get poly to raise the exception to toplevel in a more timely fashion?
Thanks
Tom
---------- Forwarded message ---------- From: Tom Ridge thomas.ridge@cl.cam.ac.uk Date: 2008/5/23 Subject: Re: [polyml] Re: Interactive behaviour and ctrl-c To: Michael Norrish Michael.Norrish@nicta.com.au Cc: hol-developers@lists.sourceforge.net
Dear All,
I've just tried this simple experiment in poly's top-level:
fun f x = 1 + f x;
f 1;
(* leave this to run for 10 or 20 seconds *)
(* type ctrl-c *)
(* type f to raise an exception *)
(* now wait while the exception is raised... this takes a while *)
So it seems that the slow-ctrl-c behaviour is something to do with (64bit) poly, and not HOL. Can someone confirm that this *doesn't* happen under 32bit poly (linux and Mac).