On Tue, 29 Apr 2014, Andreas Lochbihler wrote:
* What are your exact hardware parameters: CPU, main memory?
Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory
That is a recent high-end laptop or a midrange desktop machine.
JinjaThreads is *the* biggest Isabelle application on the planet, it
deserves a proper workstation or server, lets say with 8 cores and 16 GB
minimum (which is still small by today's standards).
ML_PLATFORM="x86-linux"
ML_HOME="~/.isabelle/contrib/polyml-5.5.1-1/x86-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
That is OK for batch mode, but in interactive mode the GC time of the
Poly/ML RTS will be quite noticable.
I will make a few experiments with x86_64 and some real memory beyond 16
GB, and report my experience later.
* What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
JEDIT_JAVA_OPTIONS ?
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4
-Dactors.enableForkJoin=false"
This looks OK for that situation. Note that you can strip the "actors"
properties, since I have removed that altogether some days ago (e.g.
326e8a7ea287). The new JVM thread pool is hardwired to the *virtual*
number of CPU cores, which is a bit high by default, but it is not used
very much in Isabelle/Scala.
* What are the options "threads" and "parallel_proofs" ?
threads = 0, parallel_proofs = 2
Here we have the standard overloading / overheating of Intel hyperthreaded
CPUs. I reckon that most users have that problem, and experience bad
reacticity that I never see myself, because I know more about multicore
system tuning.
The maximum that makes sense on this hardware is threads = "4", as well as
ML_OPTIONS="-H 500 --gcthreads 4"
In the next Poly/ML release, David Matthews provides the means to have
this as default.
Makarius_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
