[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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