Re: [isabelle] run-away Isabelle process
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:
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.
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 things.
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?
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.
> 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.
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
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.
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
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 that.
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.
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 completion.
This archive was generated by a fusion of
Pipermail (Mailman edition) and