[isabelle-dev] sledgehammer

[Jasmin Christian Blanchette]

Am 03.10.2013 um 12:08 schrieb Tobias Nipkow <nipkow at in.tum.de>:

> With Isabelle/jedit (566b769c3477) I get
> 
> "remote_vampire": Error: SystemOnTPTP is currently not available: ERROR: Cannot
> make temp dir /tmp/SystemOnTPTPFormReply634.
> 
> "remote_e_sine": Error: SystemOnTPTP is currently not available: ERROR: Cannot
> make temp dir /tmp/SystemOnTPTPFormReply634.
> 
> It looks like the problem is on the SystemOnTPTP side, I am just posting this in
> case it is a last minute problem on our side.

This is almost certainly a problem on the SystemOnTPTP side (hence the cc). The "/tmp" directory seems to get full there every six months or so. Telling Geoff is usually enough to make the problem vanish.

Jasmin