Re: Is remote ATP solving server now down?

MML version 5.29.1227 is now installed on the MizAR ATP server, so
remote ATP solving should work in Emacs too.
Josef

On Sat, Feb 21, 2015 at 4:57 PM, Boris Schminke <[email protected]> wrote:
> 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