Email Gateway (Aug 19 2022 at 12:37): Email Gateway (Aug 19 2022 at 12:37):From: Makarius <makarius@sketis.net>
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?
It has been Sledgehammer that I've mainly associated that with, but
today, I was using the command "export_code" in a simple theory, which I
include below.
I would say that Sledgehammer and export_code are quite different. I did
see occasional left-over process from Sledgehammer on Windows, notably E
prover, but that is not poly.exe.
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.
With Isabelle2013, rarely did processes get started that weren't
terminated.
In principle, I made several things in the process management more robust.
Some of that could cause new problems nonetheless.
Isabelle2013-1 also has an updated version of Cygwin, which could in
principle be less reliable than the one we've had before. This has
happened before, but so far there is no proof for that.
After I closed jEdit, a bunch of processes terminated, including a poly.exe,
but these 4 processes were still running:poly.exe
env.exe
bash.exe
bash.exe
This looks like the normal collection of processes for the prover backend.
Normally, stopping jEdit and its Isabelle/jEdit plugin should terminate
the processes as well. There is also a global JVM shutdown handler:
regular termination of the Java runtime should dispose any add-on
processes.
This does not work though, if the JVM is in bad state and needs to be
terminated the hard way, i.e. the light is switched of with the hammer.
Makarius
Email Gateway (Aug 19 2022 at 12:37):From: Gottfried Barrow <gottfried.barrow@gmx.com>
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.
Regards,
GB
Email Gateway (Aug 19 2022 at 12:38):From: Makarius <makarius@sketis.net>
So far I did not have the impression that you economize the character
counts of your text :-)
"PIDE" is fine -- it is the umbrella term for the "Prover IDE" concepts
and implementations, and covers all particular implementations, e.g.
Isabelle/jEdit, Isabelle/Eclipse (Newcastle), clide (Bremen).
The confusion of the "Isabelle/jEdit" prover IDE with the "jEdit" text
editor is particularly critical, since "jEdit" is a well-known brand in
certain communities. Posting about Isabelle/jEdit on Stackoverflow or on
the jedit mailing lists, but calling it just "jEdit" would cause
unnecessary problems.
And yes, Isabelle/jEdit adds so much to the basic jEdit substrate that it
deserves its own branding. (I did not anticipate so much extra work when
I started the project around 2008.)
Makarius
Email Gateway (Aug 19 2022 at 12:38):From: Makarius <makarius@sketis.net>
OK, I have learned something about 'export_code': using SML as target
language seems to run a separate Isabelle/ML process to check the result.
(In your example you've hand only Scala and Haskell, though.)
I have experimented with export_code in SML myself, but did not manage to
see left-over processes after 10-20 times reloading of the example theory
(Windows 2008, 4 cores).
Since you see poly.exe processes in particular, there might be a new
problem introduced in the way I start Poly/ML 5.5.1 in Isabelle2013-1,
instead of Poly/ML 5.5.0 in Isabelle2013. This is just another theory, as
alternative to postulate a problem with the Cygwin update.
To try it yourself, you can downgrade Isabelle2013-1 to Poly/ML 5.5.0 as
follows:
* Open $ISABELLE_HOME/etc/components in Isabelle/jEdit (the file name
can be typed like that in the file browser).
* Replace the line "polyml-5.5.1-1" by "polyml-5.5.0-3" (without
touching anything else).
* Quit Isabelle/jEdit and run Isabelle2013-1\Cygwin-Terminal.bat
* On the command line run "isabelle components -a", which will download
and unpack the requested Poly/ML version.
Now you can close the terminal and restart Isabelle/jEdit -- it will
rebuild your standard logic image, which is normally "HOL". In this new
situation, the starting of external poly.exe processes works more like in
Isabelle2013.
Makarius
Email Gateway (Aug 19 2022 at 12:38):From: Gottfried Barrow <gottfried.barrow@gmx.com>
On 11/23/2013 5:42 AM, Makarius wrote:
So far I did not have the impression that you economize the character
counts of your text :-)
A novelist culls down 100,000 words to 40,000 words, which is not
apparent to others, because the 40,000 words still exists. The value of
the 40,000 words is sometimes only of internal value to the writer.
For my question about code generation about Trueprop, I actually worked
to limit its length. Brevity becomes important when one wants to
increase the chances, from 5% to 6%, that busy people will take time to
read past the first paragraph.
"PIDE" is fine..
And yes, Isabelle/jEdit adds so much to the basic jEdit substrate that
it deserves its own branding. (I did not anticipate so much extra
work when I started the project around 2008.)
Economy dictates that I should leave off suggesting a major rebranding
of Isabelle, to that of the IsaSuite, which would include the products
IsaML and IsaJEdit, where, of course, there's no need for IsaIsar, as
it's readily seen that's there's an isa in the Isar.
To not economize my words is to dilute their value, and some kind of
rebranding is inevitable anyway. It always happens after the IPO. The
stock price eventually goes down. The corporate board, looking for
solutions, fires the principals who started it all. As to whether there
will be a Steve Jobs'ish comeback, only time will tell. Cursing,
screaming, and yelling by the principals should begin now, or the
storyline will suffer.
On 11/23/2013 8:15 AM, Makarius wrote:
I have experimented with export_code in SML myself, but did not manage
to see left-over processes after 10-20 times reloading of the example
theory (Windows 2008, 4 cores).Since you see poly.exe processes in particular, there might be a new
problem introduced in the way I start Poly/ML 5.5.1 in Isabelle2013-1,
instead of Poly/ML 5.5.0 in Isabelle2013. This is just another
theory, as alternative to postulate a problem with the Cygwin update.To try it yourself, you can downgrade Isabelle2013-1 to Poly/ML 5.5.0
as follows:...
With the latest release, these non-terminated processes have come during
an initial flurry of experimenting to try and figure out how things
work, which generally falls under the category of "problems due to
trying to make Windows do too much at one time".
I'm not having problems now, but then, I'm not demanding much of the
PIDE because I've got done what I wanted. Surely, though, it was related
to export_code because the file was so small, and commenting in and out
"export_code" was about all I was doing.
I guess I'll hold off on making the changes you suggest. Right now, I'm
not having any problems, so I wouldn't know if it fixed anything.
From the time I was studying the processes of Sledgehammer, my notes
show that metis is run by poly.exe, and metis is called by different ATPs.
Also, the extra poly.exe I mentioned was because I had an additional
view open in the PIDE, which I forgot about. When I closed it, the
poly.exe was terminated.
Lots of poly.exe's get called. With Isabelle2012 (or Isabelle2011-1),
something like eprover.exe would be left running sometimes, but I don't
think I've seen that lately.
I won't be putting many demands on the PIDE for months, because I'm
trying to learn Scala, so that will limit what problems I can discover,
and these unpredictable problems could go away in that time.
Regards,
GB
Email Gateway (Aug 19 2022 at 12:38):From: Makarius <makarius@sketis.net>
On Sat, 23 Nov 2013, Gottfried Barrow wrote:
From the time I was studying the processes of Sledgehammer, my notes
show that metis is run by poly.exe, and metis is called by different
ATPs.Also, the extra poly.exe I mentioned was because I had an additional
view open in the PIDE, which I forgot about. When I closed it, the
poly.exe was terminated.
Note that the Prover IDE is connected to a single Isabelle/ML process
(poly.exe) the whole time. Multiple editor views, buffers etc. don't
matter. Things are different when you run multiple Isabelle.exe Windows
applications at the same time, of course.
Metis is always run internally in the same prover process as anything
else.
SML export_code runs a different, isolated poly.exe each time it is
invoked.
Lots of poly.exe's get called. With Isabelle2012 (or Isabelle2011-1),
something like eprover.exe would be left running sometimes, but I don't
think I've seen that lately.
I still do see stray eprover processes, also on Unix platforms. This is
probably a remaining problem of Stephan Schulz.
Makarius
Email Gateway (Aug 19 2022 at 12:42):From: Makarius <makarius@sketis.net>
A few more remarks, after looking once again over the external process
management of Isabelle/Scala and Isabelle/ML.
Process management according to POSIX only allows flat (non-nested)
process groups and asynchronous (unacknowledged) signals to kill another
process. To give the appearance of managed hierarchies of processes, the
Isabelle framework implements certain common-sense heuristics that usually
work, but implicitly depend on a reasonable degree of reactivity.
Under heavy load, though, a process that is signalled to terminate, but
remains unresponspive for too long, is killed the hard way. Thus it has
no chance to terminate its sub-processes properly.
This explains why an abrupt termination of the outermost PIDE application
can leave some external processes at the bottom of the hierarchy behind.
Makarius
Email Gateway (Aug 19 2022 at 12:42):From: Lars Noschinski <noschinl@in.tum.de>
I recently learned that recent linux kernels (>=3.4) allow setting the
PR_SET_CHILD_SUBREAPER flag on a process. Basically this means that all
(indirect) children of this process will be reparented to it instead of
PID 1, when their parent dies.
So this would allow better management of processes, but is of course not
yet very portable. I would be willing to investigate this further, if
there is any interest in that.
-- Lars
signature.asc
Email Gateway (Aug 19 2022 at 12:42):From: Makarius <makarius@sketis.net>
Linux has many interesting things that are not generally known nor used.
Linus Torvalds has recently given an interview with two notable points:
(1) most people ignore the really good things of the Linux kernel -- for
portability reasons, and (2) Linux desktop projects are all really bad,
and the continuous forking of projects works against the whole movement
towards total world domination.
Anyway, when I say "POSIX", it means the intersection of Mac OS X, Windows
Our multiplatform hints and guidelines
http://isabelle.in.tum.de/repos/isabelle/file/Isabelle2013-1/Admin/PLATFORMS
refer to Ubuntu 10.04 LTS as the reference platform to build Isabelle
components for Linux. This means, before every Isabelle release I need to
boot up certain virtual machines to check things or recompile some add-on
tools.
Doing it this time, I was just surprised how nice and stable Ubuntu 10.04
was compared to current versions (not just Ubuntu, also other Linux
distributions). I still need to get my own machine back into shape, and
will probably try Centos next. (At the danger of missing messed-up
Debian/Ubuntu packages of basic Unix tools the next time.)
Makarius
Email Gateway (Aug 19 2022 at 12:55):From: Makarius <makarius@sketis.net>
This should be resolved in Isabelle2013-2-RC3 -- I won't blame Stephan
Schulz again for his creative signal handlers in the C code of E Prover.
As long as you stay within Isabelle/jEdit, external processes should be
terminated eventually. When you close the Windows application while the
prover process is really busy with external loads, there is the old danger
of dangling tail ends of such processes.
What is missing here for future releases: a proper PIDE application
shutdown phase that notiates with the prover process via the PIDE
protocol, not crude POSIX signals.
Makarius
Email Gateway (Aug 19 2022 at 13:08):From: Makarius <makarius@sketis.net>
This side-remarked greatly helped to figure out that a paractical problem
was still remaining, until I addressed that in the present
Isabelle2013-2-RC3 --- 2 days left for testing.
Makarius
Last updated: Apr 20 2024 at 04:19 UTC