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
/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/recode.pl" "$MLTEXT")" --error-exit < /dev/null
failed to remove
Directory not empty
Return code: 134
This archive was generated by a fusion of
Pipermail (Mailman edition) and