[isabelle] Sledgehammer - Cannot connect to server · Archive Mirror: Isabelle Users Mailing List

Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Sledgehammer - Cannot connect to server

Email Gateway (Aug 22 2022 at 10:20):

From: Artur Gomes <gomesa@tcd.ie>
Hi there,

I'm starting using Isabelle and I tried to find the answer looking back at
the mailing list history but I couldn't find anything related to it.
Well, I'm trying to run the "sledgehammer" but I get the following message:

Sledgehammering...
Cannot connect to server.
"remote_vampire": Error: SystemOnTPTP is not available.

Could someone give me some tips of what should I do in order to configure
my computer to use the online service? Just to make clear, it is working
for local solutions anyway.
By the way, I'm running Isabelle 2015 on OS X 10.10 (Yosemite).

Thank you very much indeed.

Best wishes,

Artur

Email Gateway (Aug 22 2022 at 10:20):

From: Larry Paulson <lp15@cam.ac.uk>
Welcome to the group!

I suspect that you haven’t done anything wrong. Rather, the SystemOnTPTP service at Miami appears to be down. You can still use sledgehammer with provers installed on your machine, as long as it is powerful enough. Unfortunately, Vampire is not available for download at the moment either; possibly it will be after CADE in August.

Larry Paulson

Email Gateway (Aug 22 2022 at 10:20):

From: Makarius <makarius@sketis.net>
What often helps in such situations are masses of users telling the author
of such a tool to release it under a proper open-source license.

Even the MS empire has eventually done that, and released Z3 in a manner
that it could be included in Isabelle2015 for everyone to use freely.

Makarius

Email Gateway (Aug 22 2022 at 10:21):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
Makarius wrote:

Indeed, I have brought this up on a number of occasions, including at my invited Vampire 2014 talk (pp. 3-4):

http://www.loria.fr/~jablanch/life.pdf

Andrei and Laura told me they will happily provide binaries to anybody if they ask by email.

Since we now have a good collection of local provers (CVC4, E, SPASS, Z3), we do not need to rely on external provers by default, at least on 4-core machines. I have made a change to that effect in the repository (a9b71c82647b).

Jasmin