[isabelle-dev] sledgehammer

[Geoff Sutcliffe]

Hi,

> > 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.

I have cleaned out. Please try again, and let me know if you have further
problems. Sledgehammer is hammering like crazy these days!

Cheers,

Geoff

Geoff Sutcliffe                           http://www.cs.miami.edu/~geoff
Department of Computer Science            Email : geoff at cs.miami.edu
University of Miami                       Phone : +1 305 2842158/2842268
(Director of Undergraduate Studies)       FAX   : +1 305 2842264
----- "My cat" is not a float. Every string should learn to swim. ------