Re: Is remote ATP solving server now down?

Thank you! :)
21 февр. 2015 г. 18:52 пользователь "Josef Urban" <[email protected]>
написал:

> Hi Boris,
>
> the line:
>
> sh: bin5.29.1227/mizf: not found
>
> suggests that version 1227 is not installed on the MizAR server yet
> (you can check this by looking at the available MML versions at
> http://mizar.cs.ualberta.ca/~mptp/MizAR.html ).
>
> I can see at ftp://mizar.uwb.edu.pl/pub/system/i386-linux/ that the
> linux version of 1227 was released a week ago, so I'll install it at
> the server soon (probably next week).
>
> Josef
>
>
>
> On Sat, Feb 21, 2015 at 12:37 PM, Boris Schminke <[email protected]>
> wrote:
> > I try to use "by;" trigger for remote solving. I use this correct
> article as
> > a test-case:
> >
> > environ
> > begin
> > 1=1;
> >
> > But when I try (in Emacs with Mizar mode) to type by; instead of ; to
> > auto-complete proof I receive the following message:
> >
> > ATP-Unsolved; :: [ATP details]
> >
> > and the details are:
> >
> > HTTP/1.1 200 OK
> > Date: Sat, 21 Feb 2015 11:36:00 GMT
> > Server: Apache/2.2.20 (Ubuntu)
> > Vary: Accept-Encoding
> > Keep-Alive: timeout=5, max=100
> > Connection: Keep-Alive
> > Transfer-Encoding: chunked
> > Content-Type: text/html; charset=ISO-8859-1
> >
> > sh: bin5.29.1227/mizf: not found
> >
> > ==========
> >
> > ==========
> >
> > ==========
> >
> > ==========
> > Request took 0s
> >
> > Any ideas?
> >
> > Regards,
> > Boris
>