Re: [isabelle] Stray processes on Windows



On Fri, 22 Nov 2013, Gottfried Barrow wrote:

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.

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




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