Re: [isabelle] Sledgehammer - Cannot connect to server



Hi all,

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

It turns out SystemOnTPTP has moved to a new URL. If you want it to work again, you will need to change the file

    src/HOL/Tools/ATP/scripts/remote_atp

replacing

  "http://www.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReplyâ;;

with

  "http://pages.cs.miami.edu/~tptp/cgi-bin/SystemOnTPTPFormReplyâ;;

This is a Perl script. You will *not* need to rebuild anything so that the change takes effect. This will be fixed in the next Isabelle version.

Thank you for your report!

Regards,

Jasmin





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.