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