Re: [isabelle] RC4: sledgehammer on Cygwin crashed once; temp file not removed

On 14-08-26 04:05, Makarius wrote:
That is one of these hard crashes of the Poly/ML runtime system that become the more likely the more it approaches certain resource limits.

Finally another crash.

This is following a pattern. The crash doesn't happen until after I terminate the sledgehammer command, and then it's not immediate.

In this case, I haven't changed threads back to threads=4, it's still at 12, with the 17 provers.

About 30 seconds after I terminated a sledgehammer command, I was staring at the screen thinking about what I wanted to do, and it terminated. The "Isabelle Syslog" message is below:


Welcome to Isabelle/HOL (Isabelle2014-RC4: August 2014)
assertion "baseAddr > (PolyWord*)obj && baseAddr < ((PolyWord*)obj)+length" failed: file "gc_mark_phase.cpp", line 439, function: virtual void MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*, POLYUNSIGNED)

message_output terminated
/cygdrive/e/E_2/dev/Isabelle2014/lib/scripts/run-polyml-5.5.2: line 84: 6368 Aborted (core dumped) "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/" "$MLTEXT")" --error-exit < /dev/null


failed to remove
Directory not empty

standard_output terminated
standard_error terminated
process terminated
command_input terminated
process_manager terminated
Return code: 134

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