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.