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

[Jasmin Christian Blanchette]

Am 24.04.2012 um 20:27 schrieb Jasmin Christian Blanchette:

> I can reproduce it on my WinXP-on-VirtualBox installation. There are a couple of variants of this: Sometimes it affects a remote prover, sometimes I get an "empty string" error from "remote_e". It's certainly not tied to "spass". The error seems to go away when an explicit prover is specified by passing "[prover = ...]" to the "sledgehammer" command.

Update: I couldn't track it down with 100% certainty, but I strongly suspect that the "Empty" exception stems from the "split_last" call in "sledgehammer_provers.ML", which extracts the timing value output by the Unix "time" command. There's an assumption lurking in there that the output of "time foobar" will be at least one line long, which seems reasonable but appears to be violated by Isabelle on Cygwin once every so often. There appears to be something fishy going on with parallel "bash_output" calls.

In any case, I've now made the code more robust to at least avoid the exception (change 63c939dcd055).

Jasmin