Re: [mizar] Re: Mizar Proof Advisor

[Boris Schminke <schminkeba@gmail.com>]

Dear Josef,
I use GNU Emacs 23.2.1 (i686-pc-linux-gnu, GTK+ Version 2.24.4) and
the MML 7.12.01 1132. Maybe my .emacs file is wrong somehow, because I
took it from Windows Mizar distribution. I haven't found it in the
Linux one.

On 25 August 2011 11:36, Josef Urban <josef.urban@gmail.com> wrote:
> Dear Boris,
>
>
> On Thu, Aug 25, 2011 at 9:10 AM, Boris Schminke <schminkeba@gmail.com> wrote:
>> Deal All,
>> I understood than there is little need for MPA now when remoted ATP
>> solving is available.
>
> The old MPA server should be up again now. Indeed, it can be improved
> significantly by more detailed proof analysis and better machine
> learning methods, I hope to have a new instance of it this or next
> week.
>
>> But I've faced another problem: while trying to
>> generate proof sceleton Emacs hungs up (running under Windows 7 or
>> Ubuntu 11). Please help!:)
>
> Can you send me a small example, version of your MML, and the (Ubuntu)
> version of Emacs you are using?
>
> Best,
> Josef
>
>>
>> On 22 August 2011 16:26, Boris Schminke <schminkeba@gmail.com> wrote:
>>> Dear All,
>>> Is MPA server down only for a while or I've missed something important?
>>>
>>> Yours,
>>> Boris.
>>>
>>
>> --
>> Yours,
>> Boris.
>>
>

-- 
Yours,
Boris.