[isabelle-dev] Remaining uses of Proof General?
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 ?
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