Re: [isabelle] Greyout followed by gc error
For me it looks like there is some bug in the PolyML garbage collector,
which is likely to be triggered under heavy parallel load. David??
I get this assertion sometimes (3 times in the last month) if I open a
theory that depends on a whole bunch of new theories.
My machine is
Intel(R) Core(TM) i7-2720QM CPU @ 2.20GHz with 4 cores (i.e. 8 cores
with hyperthreading), with 8GB of RAM
On Mi, 2015-01-14 at 16:40 +0100, Joachim Breitner wrote:
> I just had a greyout followed, after a while, by this message:
> Welcome to Isabelle/HOLCF-Nominal2 (Isabelle2014: August 2014)
> poly: gc_mark_phase.cpp:439: virtual void MTGCProcessMarkPointers::ScanAddressesInObject(PolyObject*, POLYUNSIGNED): Assertion `baseAddr > (PolyWord*)obj && baseAddr < ((PolyWord*)obj)+length' failed.
> Malformed message:
> bad chunk (unexpected EOF after 136 of 618 bytes)
> message_output terminated
> /opt/isabelle/Isabelle2014/lib/scripts/run-polyml-5.5.2: Zeile 84: 7181 Abgebrochen "$POLY" -q -i $ML_OPTIONS --eval "$(perl "$ISABELLE_HOME/lib/scripts/recode.pl" "$MLTEXT")" --error-exit < /dev/null
> standard_error terminated
> standard_output terminated
> process terminated
> command_input terminated
> process_manager terminated
> Return code: 134
> This happened during a refactoring phase, where I have a number of
> „target“ theories ticked in the theory panel, which obviously puts some
> strain on the system. I was disabling and enabling the global
> „Continuous checking“ parameter before, which might be related.
> This is a Intel(R) Core(TM) i7-3520M CPU @ 2.90GHz machine with 4 cores,
> 8GB or RAM.
This archive was generated by a fusion of
Pipermail (Mailman edition) and