Re: [isabelle] run-away Isabelle process



Thank you, Thomas.  I will add these to my set of options.
---Elsa


On 5/3/15 8:50 PM, Thomas Sewell wrote:
Hello Elsa.

I'm not completely sure about this, but I have taken the following
actions a couple of times and I *think* they might have reduced polyML's
memory footprint.

1) Restart Isabelle if polyML is getting too big. I am anecdotally
convinced that sometimes polyML's heap size drifts upwards over time,
and that a restart can reset this.

2) Try enabling "skip-proofs" during the reset while rebuilding up to
where you were before. You can find an option for skipping proofs in
Isabelle's options panel: jEdit menu Plugins->Plugin Options, pick
Isabelle->General, find the skip proofs setting. This will not only save
time, it will cause polyML to build less proof-related objects
internally, which may save memory.

Caveat emptor ; all of the above may simply be a superstitious ritual I
go through as a result of confirmation bias.

Good luck,
    Thomas.

On 04/05/15 09:18, Elsa L. Gunter wrote:
Dear Makarius,
  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:

659   poly403.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:

623   JavaAppLaunc 0.1   19:47.99 65   7    333   2179 280M+
307M+ 0B

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?
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
Plugin
 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
that.

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.

    Makarius

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.
---Elsa





________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.