Re: [mizar] Re: Mizar Proof Advisor

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

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.
>