[isabelle-dev] Remaining uses of Proof General?

[Andreas Lochbihler]

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