Re: [mizar] Is remote ATP solving server now down?

[Josef Urban <josef.urban@gmail.com>]

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 <schminkeba@gmail.com> wrote:
> Thank you! :)
>
> 21 февр. 2015 г. 18:52 пользователь "Josef Urban" <josef.urban@gmail.com>
> написал:
>
>> 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 <schminkeba@gmail.com>
>> 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