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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
