Your previous message got me enough wiggle room to get the immediate
theorm I was working on to go through.
On 5/3/15 3:48 PM, Makarius wrote:
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+
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+
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
I don't see java itself showing up. I think polyml is the hog.
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?
Almost. There is a in List-Inifinite that needs to be included
because of some reorganizing of the AFP entry. Everything I need from
JinjaThreads is in my precompiled heap.
> 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 > is.
That could be outdated_color. You can change the color value in
Options / Isabelle / Rendering to check this hypothesis.
Which field should I change? There are several greys, and my eyes
aren't good enough to tell them apart.
The left column has all colors in alphabetical order. There should
be an entry "Outdated color" with some pinkish grey.
OK. I have changed it to a kind of light lime green that I think I
will not confuse with anything else. Since it isn't choking yet
(although it still runs at 200% CPU with over 8 GB of memory when I
have not requested it to do anything), I cn't tell it tha tis the
color of a choke.
Just what is Isabelle (polyml) doing when the cursor is sitting at the
end of a fully successfully completed proof? I would have expected it
to be waiting for user input before doing anything else, but it keeps
running something. The energy impact of Isabelle is over ten times
more than everything else on my system combined, and I'm lazy about
leaving stuff around.
It 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 nicely.
I have not found all the sources of the ambiguities, but loading two
different theories that sue syntax that is unambiguous in itself can
lead to ambiguous syntax. Since there are no checks the mixfix syntax
has been done right, it would be nice to have a way of pretty printing
that was guaranteed to parse. Shutting off mixfix I believe would do
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.
Thank you for your help and your offer for more. I hope/think I can
now limp through the next week. However, this has caused me to wonder
how I can continue to use Isabelle for the project on which I am
embarked. I am only at the beginning and if I am running out of
resources now, I'm not sure how I could hope to carry my project to