[mizar] verifier infinite loop

[Jesse Alama <alama@stanford.edu>]

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

I deleted all the auxiliary files associated with my article and re-ran
the verifier, but I got the same behavior.

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.

What's puzzling is that with an earlier MML I was checking my article
just fine.  What might be going on?

Thanks,

Jesse

-- 
Jesse Alama (alama@stanford.edu)
*121: Disagreement of argument types (http://www.mizar.org)