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 -?" ?
ML_PLATFORM="x86-linux"
ML_HOME="~/.isabelle/contrib/polyml-5.5.1-1/x86-linux"
ML_SYSTEM="polyml-5.5.1"
ML_OPTIONS="-H 500"
* What are your JVM settings: ISABELLE_JAVA_SYSTEM_OPTIONS and
JEDIT_JAVA_OPTIONS ?
JEDIT_JAVA_OPTIONS="-Xms128m -Xmx3072m -Xss2m -Dactors.corePoolSize=4
-Dactors.enableForkJoin=false"
* What are the options "threads" and "parallel_proofs" ?
threads = 0, parallel_proofs = 2
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
