Re: [mizar] Re: Mizar Proof Advisor

[Boris Schminke <schminkeba@gmail.com>]

Thanks, Josef!
Automatic generation of proof skeletons is one of the coolest
Mizar-mode's features!

On 25 August 2011 12:12, Josef Urban <josef.urban@gmail.com> wrote:
> Dear Boris,
>
> On Thu, Aug 25, 2011 at 10:01 AM, Boris Schminke <schminkeba@gmail.com> wrote:
>> 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.
>
> Yes. It seems that the new Mizar 7.12.01 has broken the lisppars
> utility, and hence the skeleton creation. I wish there was some
> standard regression testing of such utilities before a new Mizar
> version is released.
>
> I'll have a look what happened.
>
> Best,
> Josef
>
>
>>
>> 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.
>>
>
-- 
Yours,
Boris