Re: [mizar] Re: Mizar Proof Advisor

[Boris Schminke <schminkeba@gmail.com>]

Dear Josef,
what for example, it could be any

environ
begin
reserve x, y for set;

x in y

select the last line, press Ctrl-C S and wait forever.

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.