[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Mon Apr 28 23:18:45 CEST 2014
On Mon, 28 Apr 2014, Andreas Lochbihler wrote:
> 2. Reactivity when processing large files
> With PG, I knew how to control the Isabelle prover. When I edit a large
> file in a larger project like JinjaThreads, every now and then, Isabelle
> changes the background colour from red to gray and then, apparently
> nothing happens for minutes before Isabelle turns it red again and
> starts reprocessing. Is there some way to explicitly tell Isabelle that
> it should now start to check again. Toggling "continuous checking" does
> not help. Sometimes, I even have to close the theory file and reopen it
This sounds like the Poly/ML RTS is desparately trying to reclaim memory,
by aggressive sharing huge amounts of data. Not long ago that situation
lead into real memory problems on my good old 32 GB machine, but David
Matthews managed once again to postpone the ultimate JinjaThreads
implosion as a black hole of computing resources.
For now just the usual game, according to Tim the Enchanter:
* What are your exact hardware parameters: CPU, main memory?
* What is your operating system?
* What are your ML system settings, e.g. as shown by "isabelle build -?" ?
* What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
* What are the options "threads" and "parallel_proofs" ?
More information about the isabelle-dev