[isabelle-dev] "spass": Internal error: exception Empty raised (line 458 of "library.ML")
makarius at sketis.net
Fri Apr 27 23:51:12 CEST 2012
On Tue, 24 Apr 2012, Makarius wrote:
> I have also made some more experiments. The Empty exception is from the
> split_last here
> 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.
More information about the isabelle-dev