Re: [isabelle] run-away Isabelle process
On Sun, 3 May 2015, Elsa L. Gunter wrote:
Using the Activity monitor, it is primarily poly that is primary resource
hog. It is running at ~ 400% - 450~ cpu. If I run top -o cpu for a second
or two and redirect the output to a file, poly will always exactly occur once
near the top:
[11d659 poly[11;20H403.8 81:49:39 14/4 0 28 12133 12G+ 12G- 0B
Here we see 12G already, which means Poly/ML is practically at the maximum
of your 16GB machine.
and JavaAppLaunc occurs repeatedly, lower down:
[19d623 JavaAppLaunc 0.1 19:47.99 65 7 333 2179 280M+ 307M+
I can't say on the spot if this is the actual JVM run-time system. It
might be just the launcher, and a second big "java" process is elsewhere.
Normally the Prover IDE requires a few GB for such big things.
I'm not actually taking all of JinjaThreads, but cherry picking the
concurrency parts, since I'm not actually doing anything with Jinja/Java in
this project (although I am in another).
OK. Do you have all that base material in the base heap image? Or is it
loaded into the Prover IDE interactively?
> When Isabelle is semi-non-responsive, it usually colors all of the text
> grey (not purple). I haven't been able to tell which of the greys it
Which field should I change? There are several greys, and my eyes aren't
good enough to tell them apart.
That could be outdated_color. You can change the color value in Plugin
Options / Isabelle / Rendering to check this hypothesis.
The left column has all colors in alphabetical order. There should be an
entry "Outdated color" with some pinkish grey.
I would be useful if I could shut off the pretty printing for mixfix as
well so that isabelle could parse what it prints. I have shut off
abbreviations, but i have not found a flag for the mixfix.
If it is your own mixfix syntax, you could specify an explicit print mode
and turn that on/off on demand. But I don't think that is needed: doing
mixfix syntax right, without ambiguities, it should parse and print
We are only borrowing the theory of bisimulation from JinjaThreads, not
the whole Jinja concurrent semantics. bisimulation alone is big, but I
thought it was less than a quarter of all of JinjaThreads. I could be
wrong, but I think the total code I'm adding on top of bisimulation is
less than the amount I have left out of JinjaThreads.
This sounds quite reasonable. JinjaThreads contains many interesting
things, well-hidden to potentially interested parties.
If you want, you can send me your development privately, so that I can
experiment with it a bit on my modest 12 core, 32 GB machine.
This archive was generated by a fusion of
Pipermail (Mailman edition) and