Am 23.04.2012 um 22:02 schrieb Makarius: > On Mon, 23 Apr 2012, Alexander Krauss wrote: > >> Sledgehammering... >> "spass": Internal error: >> exception Empty raised (line 458 of "library.ML") >> >> "remote_vampire": Try this: by metis (12 ms). >> "remote_e_sine": Try this: by metis (13 ms). > > I've seen it before, but for the remote provers, and did not investigate > further yet. My first idea was it could be a problem of the network > connection of the heavily fortified vmbroy9 machine, but spass is certainly > local.
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. I'll see if I can debug this further. I can't seem to get this to happen with the Mac bundle (from 23 April 2012). Jasmin _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
