[Date Prev][Date Next]
[Chronological]
[Thread]
[Top]
Re: [mizar] verifier infinite loop
On Sat, 21 Apr 2007, Jesse Alama wrote:
I tried running the mizar verifier (as distributed in version 7.8.04 of
the binaries) on an article which, I believe, I hadn't verified since
the last change to to the MML (from 4.80.959 to 4.81.962). There were
some errors having to do with the change of "1." to "1_", and I got rid
of those, I believe. But, to my surprise, it looks like the verifier is
now unable to finish its job on my article: the verifier never
terminates. I'm running the Mac OS X darwin/ppc binary.
Each time I interrupt it the only error is *1255 ("Ctrl break").
The error should be reported in the line which runs wild - try commenting
it out and see if the file can be verified then.
I deleted all the auxiliary files associated with my article and re-ran
the verifier, but I got the same behavior.
It would be good to check if this can also be reproduced on a different
system.
I checked out the .log file associated with my article and found some
messages suggesting that some constructors were missing, and I added all
the missing constructors mentioned there, but still I get an infinite
loop.
The *.log file is created by the accommodator, not the verifier, so that
was unnecessary.
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...
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/
======================================================================