[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Tue Apr 29 16:46:27 CEST 2014
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_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
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
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.
More information about the isabelle-dev