Re: [mizar] Re: Mizar Proof Advisor

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

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