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


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