Re: Re: Mizar Proof Advisor

Boris Schminke <[email protected]>
Newsgroups gmane.comp.mathematics.mizar
Message-ID <CAC-WUu1TqtTCRKwAMXoAA6mTboJ8ZhMFgUzjG1Q-6TdzDAcRKg@mail.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 <[email protected]> wrote:
> Dear Boris,
>
>
> On Thu, Aug 25, 2011 at 9:10 AM, Boris Schminke <[email protected]> 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 <[email protected]> wrote:
>>> Dear All,
>>> Is MPA server down only for a while or I've missed something important?
>>>
>>> Yours,
>>> Boris.
>>>
>>
>> --
>> Yours,
>> Boris.
>>
>

-- 
Yours,
Boris.
lmpx.com only provides a reader for public news (NNTP) servers. It is not affiliated with the servers or forums shown here and is not responsible for the content of articles, which is written by their respective authors.