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:

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


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


	Makarius





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