[Date Prev][Date Next] [Chronological] [Thread] [Top]

[mizar] New Mizar version/vocabularies



  Dear All,
as Artur Kornilowicz previously wrote on November 10, the revision acting mainly on MML vocabularies took place, and it can be rather
painful for active authors, especially for those who continue
their work on older articles.
  After the new version (7.11.04) of the Mizar system is installed,
you may encounter an internal error during the accomodation pass.
Nothing really to be afraid of, but probably old, incompatible
accomodation results are still stored somewhere in "text" directory.
Usually removing all files (OK, .miz should remain ;)) from
"text" directory will heal the situation. Or, alternatively, just
force the accomodation.
  As for the accomodator errors, you will probably get some *801
errors in the "vocabularies" section, marked indentifiers should be
deleted. In parallel, *830 in "notations" section means that marked
identifier is completely unused (usually ZFMISC_1, NUMBERS etc.),
so adding this to "vocabularies" will help.
  After this, "findvoc" utility for symbols which are not properly
recognized, will help.
  Note, that any article send to the Library Committee for inclusion
in the MML should be verified by the newest official version.
  Regards,
  Adam Grabowski
  Library Committee of the Association of Mizar Users