Re: [isabelle] Stray processes on Windows
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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and