[isabelle-dev] "spass": Internal error: exception Empty raised (line 458 of "library.ML")

[Makarius]

On Tue, 24 Apr 2012, Makarius wrote:

> I have also made some more experiments.  The Empty exception is from the 
> split_last here 
> http://isabelle.in.tum.de/repos/isabelle/file/ea153f6abdb6/src/HOL/Tools/Sledgehammer/sledgehammer_provers.ML#l614 
> where you don't get any output unexpectedly, bacause /bin/sh has 
> crashed. Ouch!
>
> Such things happen on Cygwin.  I will try to sort out the physical problem.

The situation is still not fully clear.  It seems that /bin/sh.exe and 
especially /bin/perl.exe tend to crash on Cygwin in the way they are used 
here with src/Pure/Concurrent/bash.ML.

I have made a plain C wrapper to replace lib/scripts/process, see 
Admin/exec_prosess -- this component can be compiled manually with the 
included build script and initialized in settings or components in the 
usual way.  The idea is to ship that in the Cygwin bundle.

Doing this for vmbroy9 seems to improve stabilit significantly.  I did not 
get any crashes of "e" or "spass" after 20..40 runs.

The remote provers still crash occasionally due to their inherent reliance 
on perl.  It seems that the best times of the rock-solid Larry Wall 
operating systems are over, at least on this slightly odd Linux variant 
with MS kernel.


 	Makarius