Re: [isabelle] 2014-RC1 issues



On 07/08/2014 08:13, Lars Noschinski wrote:
Interestingly, asking for an exception trace (via
[[ML_exception_trace]]) for this code sends polyml into a another
desperate quest for memory: It has been running on my machine a few
minutes with 4086M VIRT and 3956M RES -- so basically exhausting its
full address space -- before giving up:

     Welcome to Isabelle/HOL (Isabelle2014-RC2: August 2014)
     Warning - Unable to increase stack - interrupting thread

     Warning - Unable to increase stack - interrupting thread

     Warning - Unable to increase stack - interrupting thread

     Warning - Unable to increase stack - interrupting thread

     Run out of store - interrupting threads

     Run out of store - interrupting threads

     Failed to recover - exiting

     message_output terminated
     standard_output terminated
     standard_error terminated
     process terminated
     command_input terminated
     process_manager terminated
     Return code: 1


I would guess, and it is only a guess since I haven't actually tested this, is that there is an infinite or at least very deep recursion there. The thread stacks are expanded until the process runs out of space. The way exception-trace was done changed in Poly/ML 5.5.1. Exception_trace now builds a list of the functions rather than directly printing them to standard output as it used to. There is a problem, though, if there is no space to build the list. I don't think there is a way to limit the size of the stacks (these are the stacks of ML data managed by the Poly/ML run-time not the C stacks allocated by the system). Perhaps there should be.

David




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.