New Mizar version/vocabularies
Adam Grabowski <[email protected]>
| Newsgroups | gmane.comp.mathematics.mizar |
|---|---|
| Message-ID | <Pine.GSO.4.61.0911241351270.20214@math> |
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