Re: [isabelle] Stray processes on Windows

On 11/22/2013 4:59 PM, Makarius wrote:
On Fri, 22 Nov 2013, Gottfried Barrow wrote:

In general, I've seen that with Isabelle2013-1 and the RC versions, a poly.exe process will many times get started and never get terminated, and end up running at about 95% of the CPU.

Does that mean it is a left-over poly.exe process after you stop Isabelle/jEdit, or are there additional instances of poly.exe while you run the Prover IDE?

I'm pretty sure the two things always go together. If a poly.exe process is still running after I exit Isabelle/jEdit, it's because it got orphaned somehow when Isabelle/jEdit was running. As to "additional instances", I frequently see multiple instances of poly.exe running, sometimes starting up, and then being shut down, so I don't know under what circumstances a poly.exe process is supposed to be running. There's two running right now, and there's nothing wrong.

You go into the differences between Sledgehammer and the code generator below. All I associate these non-terminated processes to is when Isar commands stay purple for a long time; that is, that some heavy processing is going on. In the case of the code generator, it has to do a bunch of processing to generate the code, and then to write it to disk. That's all I associate it with.

(Here, I go on a "Isabelle/jEdit" tangent. In the last sentence, I had a need to refer to Isabelle/jEdit twice. The result was that the characters I used from using "Isabelle/" twice make up about 10% of the sentence. These days, I now understand that Isabelle/jEdit is a significant deviation from jEdit, and that it deserves a different name, however, there is the need for language to be efficient.

There is also the fact that you use a "path/filename" naming scheme, and it's a universal practice for people to drop the "path" in "path/filename" when the context is clear. That doesn't actually apply to me anymore because, as I said, I now understand that Isabelle/jEdit deserves a separate name from jEdit, and likewise for Isabelle/ML. As to Isabelle/Scala, I don't understand that at all, because I don't see that you've tweaked the standard distribution of Scala. I only see that you use it and distribute it.

This is sort of a complaint, but you don't need to respond to it. At this point, there are no good solutions when I have a need to refer to Isabelle/jEdit many times is a short amount of space. I can call it "it", but I need to be more explicit most of the time. I can call it "jEdit," but I know it's not supposed to be called "jEdit," because it's not "jEdit". My solution, maybe, is to start calling it "PIDE". That's 4 characters, which is efficient, as long as the meaning is clear.)

The export_code command is special since it writes out given files physically. As long as you continue typing, it will do it for several prefixes of the file name. I can't tell if this can lock up the IDE. You can try switching the new option "Continuous checking" off -- there is a checkbox in the Theories panel and a keyboard shortcut C+e ENTER. This is slightly awkward handiwork, and you must not forget to turn it on again for checking things, but it might help with occasional stateful commands.

I think these things happen more when I'm typing something new, commenting out something, or uncommenting something. Basically, when demanding processes are going back and forth between getting started and terminated, because of the three things I just mentioned, and them happening a lot withing a short period of time.

The fact that Isabelle2012 and Isbelle2013 were good at shutting down processes got me in the habit of not even thinking about causing any problems, but I can start turning the prover on and off before I do things that will invoke all these automatic processes.


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