Re: [mizar] verifier infinite loop

[Adam Naumowicz <adamn@math.uwb.edu.pl>]

On Sat, 21 Apr 2007, Adam Naumowicz wrote:

> > What's puzzling is that with an earlier MML I was checking my article
> > just fine.  What might be going on?
>
> It's really hard to say not seeing the actual source...

It seems we've managed to sort this out with Jesse - the problem was 
caused by some local library files which were not regenerated after
the MML change.

So there's a warning for other less-experienced Mizar users:

The 'makeenv' front-end to the accommodator recognizes MML changes since 
last successful accommodation, forcing new accommodation when necessary, 
but this only concerns the article being processed, not the ones it 
depends on. So if there are some files in a local library involved, they 
should all be exported (with 'miz2prel') by the user prior to running the 
main file.

Best,

Adam Naumowicz

======================================================================
Department of Applied Logic            fax. +48 (85) 745-7662
Institute of Computer Science          tel. +48 (85) 745-7559 (office)
University of Bialystok                e-mail: adamn@mizar.org
Sosnowa 64, 15-887 Bialystok, Poland   http://math.uwb.edu.pl/~adamn/
======================================================================