[isabelle-dev] Remaining uses of Proof General?

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Tue Apr 29 08:44:00 CEST 2014

On 28/04/14 23:18, Makarius wrote:
> 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?
Intel® Core™ i7-3630QM CPU @ 2.40GHz, 8GB memory

>    * What is your operating system?
Ubuntu 12.04 LTS

>    * 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="-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4 

>    * What are the options "threads" and "parallel_proofs" ?
threads = 0, parallel_proofs = 2


More information about the isabelle-dev mailing list