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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
