Re: Re: Mizar Proof Advisor
Josef Urban <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <CAFP4q15o3H7sYvYcCbSj4J6BwTvsP3PhnTqSriK1-cjx4g3Wrg@mail.gmail.com> |
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. >