Re: [isabelle] run-away Isabelle process

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.


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