Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] ITP Isabelle error


view this post on Zulip Email Gateway (Dec 20 2022 at 12:25):

From: Peter Lammich <cl-isabelle-users@lists.cam.ac.uk>
Dear List,

My student has a problem regarding sledgehammer. Might that be a
firewall issue? What does sledgehammer actually try to connect to?

view this post on Zulip Email Gateway (Dec 20 2022 at 12:42):

From: "\"Blanchette, J.C. (Jasmin Christian)\"" <cl-isabelle-users@lists.cam.ac.uk>
Dear Peter,

I don't know why the error pops up. The URL of the SystemOnTPTP service is https://www.tptp.org/cgi-bin/SystemOnTPTPFormReply.

My suggestion would be that your student specifies explicitly which provers to use and use only local provers. The need for remote provers is quite low. In fact, with Isabelle2022, by default Sledgehammer should use only local provers.

If your student is using Isabelle2022, I would be curious to see what's happening. Maybe we could have a debugging session where they share their screen with me.

Cheers,
Jasmin

view this post on Zulip Email Gateway (Dec 20 2022 at 14:14):

From: Tobias Nipkow <nipkow@in.tum.de>
On 20/12/2022 13:40, "Blanchette, J.C. (Jasmin Christian)" (via
cl-isabelle-users Mailing List) wrote:

Dear Peter,

I don't know why the error pops up. The URL of the SystemOnTPTP service is
https://www.tptp.org/cgi-bin/SystemOnTPTPFormReply
<https://www.tptp.org/cgi-bin/SystemOnTPTPFormReply>.

I get this message when use s/h and am not online.

Tobias

My suggestion would be that your student specifies explicitly which provers to
use and use only local provers. The need for remote provers is quite low. In
fact, with Isabelle2022, by default Sledgehammer should use only local provers.

If your student is using Isabelle2022, I would be curious to see what's
happening. Maybe we could have a debugging session where they share their screen
with me.

Cheers,
Jasmin


From: cl-isabelle-users-request@lists.cam.ac.uk
<cl-isabelle-users-request@lists.cam.ac.uk> on behalf of Peter Lammich
<cl-isabelle-users@lists.cam.ac.uk>
Sent: Monday, December 19, 2022 17:25
To: cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Cc: Kohlen, Bram (UT-EEMCS) <b.kohlen@utwente.nl>
Subject: [isabelle] Fwd: ITP Isabelle error

Dear List,

My student has a problem regarding sledgehammer. Might that be a firewall issue?
What does sledgehammer actually try to connect to?

--

Peter

After running a system update (including the kernel) on my machine, which runs
Linux Mint, I started to get the following error when using the sledgehammer in
Isabelle:

Failed to access SystemOnTPTP server
I/O error: Connection refused

As far as I understand, sledgehammer needs to access this server for some ATPs
that do not run locally, but so far, I could not find any solution online. Do
you have any idea why this happens? I tried reinstalling Isabelle already.
smime.p7s


Last updated: Mar 28 2024 at 12:29 UTC