[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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

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
     JEDIT_JAVA_OPTIONS ?

   * What are the options "threads" and "parallel_proofs" ?


 	Makarius