Re: [isabelle] Isabelle2014-RC0 segfault / sledgehammer raises exception DUP
On Wed, 16 Jul 2014, Lars Noschinski wrote:
Another segfault, this time triggered directly while using sledgehammer.
$ cat ~/.isabelle/Isabelle2014-RC0/etc/settings
ML_OPTIONS="-H 1000 --gcthreads 1"
JEDIT_JAVA_OPTIONS="-Xms512m -Xmx4096m -Xss4m -Dactors.corePoolSize=4
Following Makarius' suggestion, I'm leaving MaSh enabled for now, but
switch to poly 5.5.1-1 and will report on further possible crashes.
Just an update on these speculative ML_OPTIONS that I proposed to you at
ITP: "--gcthreads 1" should not make a difference, you can remove it or
use a default that makes sense for your hardware (e.g. 2 or 4). The 1 was
based on the suspicion that parallel GC could be unstable, but the
well-known ML_file editing crash was caused by SHA1.digest via ML/C FFI.
That should work better in the coming Isabelle2014-RC1.
Also note that JEDIT_JAVA_OPTIONS now have simpler defaults. You can omit
the properties for the actors framework, because it is no longer used in
There is a remaining problem that the JVM uses the full hyperthreaded
number of CPU cores by default, according to
Runtime.getRuntime().availableProcessors(), but I don't know how to change
that. Oracle is not as quick as David Matthews to adapt to current
This archive was generated by a fusion of
Pipermail (Mailman edition) and