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.


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