Email Gateway (Aug 22 2022 at 10:14): Email Gateway (Aug 22 2022 at 10:14):From: bnord <bnord01@gmail.com>
Hi,
some students of mine are complaining about the remote sledgehammer
tools not working any more. I also could reproduce this problem. Are
they gone for good, are they coming back, have they moved or is there
something funky going on?
Sledgehammer output (Isabelle2014/2015):
Sledgehammering...
Cannot connect to remote server.
"remote_vampire": Error: SystemOnTPTP is not available.
Cannot connect to remote server.
"remote_e_sine": Error: SystemOnTPTP is not available.
Best wishes
Benedikt
Email Gateway (Aug 22 2022 at 10:14):From: Larry Paulson <lp15@cam.ac.uk>
We use "System on TPTP”, a service provided by Geoff Sutcliffe of the University of Miami. Apparently we are, by far, the biggest users of this service. The link http://pages.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTP appears to be down now.
Conceivably, we shall have to provide such a service ourselves one day. The vampire prover is not available to download at the moment.
Larry Paulson
Email Gateway (Aug 22 2022 at 10:15):From: "C. Diekmann" <diekmann@in.tum.de>
Cannot connect to remote server.
"remote_vampire": Error: SystemOnTPTP is not available.
Same error here.
Conceivably, we shall have to provide such a service ourselves one day. The vampire prover is not available to download at the moment.
Even if the prover were available for download, it might be great to
have the possibility to enable some external provers. Today, a student
with a slow Macbook told me "sledgehammer does not work without
Internet".
Cornelius
Last updated: Nov 21 2024 at 12:39 UTC