Re: [isabelle] Sledgehammer - Cannot connect to server



Hi again,

Thanks Jasmin, now I get replies from 'remote_vampire' too.

Regards,

Artur

Artur

On 26 June 2015 at 10:11, Jasmin Blanchette <jasmin.blanchette at inria.fr>
wrote:

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