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
-Dactors.enableForkJoin=false"

init_component "$HOME/P/afp"
----

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 Isabelle2014.

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 hardware.


	Makarius




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