7.4 The Mizar Usage

7.4.1 Accommodate

For instance, let us assume that an article named EXAMPLE1.MIZ was created. First, we accommodate it (accommodate means to gather files and adjust them). It takes the following form to accommodate.



      ACCOM TEXTEXAMPLE1.MIZ

This accommodation reads the environment section in and gets ready for the article's demonstration by making some files of the referred article's theorems, definitions, and others that are needed by an article. Sometimes, errors may appear at this point when, for example, names of an abstract file are written incorrectly in the environment section.

Accommodation does not need to be carried out every time; however, when the environment section is changed, it needs to be accommodated again.

7.4.2 Mizar Checker

When the above is done, the Mizar checker is carried out next. To do this, the following form is needed.



       MIZAR TEXTEXAMPLE1.MIZ

When this is done, a table will appear on the screen and checks an article in the order of Parser, Analyzer, and Checker and indicates the number of checked lines and errors. If there is no error, it means that it passed the Mizar checker.



                                 PC Mizar Version 4.09


                                 Copyright (c) 1990,93 Mizar society



   Implimented by



      Andzrej Trybulec



      Czeslaw Bylinski

TEXTYA2.MIZ

Pass Line Errors Time
Parser 4870:01
Analyzer 4810:04
Reasoner4810:01
Checker12320:12

Figure 7.1: Mizar Practice Screen

7.4.3 When There Is An Error

When there is an error, the error number is entered after both ACCOM and MIZAR to an article in the form of comment by using a command called ERRFLAG.



        ERRFLAG  TEXTEXAMPLE1.MIZ

Every command can omit an extension .MIZ.

To read an error message, another file (MIZAR.MSG) needs to be viewed with an editor.

7.4.4 Useful Command

Also, there is a batch command called MIZ.BAT that is a summary of ACCOM and MIZAR. By taking the following form, accommodation and Mizar checker are carried out.



       MIZ  TEXTEXAMPLE1.MIZ

In addition, there is a more useful batch command named MIZF.BAT and when the following form takes place, it checks to see if there is any need for accommodation. When there is a need, it carries out the accommodation first and then the Mizar checker is executed.



       MIZF  TEXTEXAMPLE1.MIZ

When there are more errors, it enters the error numbers in the form of a comment to an article. At the end of an article, risen error numbers and messages are entered into a comparison table (entered comments are erased at the time when MIZF command is executed next).

7.4.5 To Call Mizar From the Editor

In addition, using exclusive macro, we can call the Mizar checker from the Multi Editor. With Multi Editor, when ALT + F5 are pressed, the Mizar checker is called and executed. In this case, because errflag is not executed, an error number will not be entered into an article in the form of comment; however, by using the + and - keys in the ten keys, a short message of an error will be shown on the upper left hand corner of the screen. By pressing the + key, the next error will be shown and on the other hand, by pressing - key, the previous error will be displayed. When there is no error, the following indication will be given.

No more errors

However, to use this device, a file called SHORT.MSG needs to be loaded.

Error numbers and a comparison table of error messages are entered into the MIZAR.MSG file under the MIZAR directory in the following form.



   # 1



   It is not true



   # 4



   This inference is not accepted



   # 9



   Too many instantiations

SHORT.MSG has its error messages written shorter than MIZAR.MSG.

Usually, when the Mizar article is written, the work involves frequent Mizar checking by dealing with one error at a time; however, by using the Multi Editor, the Mizar article can be written efficiently.

Furthermore, for exclusive Mizar macro for the Multi Editor, please contact the writer.