Re: Is remote ATP solving server now down?

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