7.4 Mizarの使い方

7.4.1 accommodate

例えば EXAMPLE1.MIZ というファイル名の article を作ったとします．まず，accomdate （アコモデート，ファイルを集めて調整するの意）します．accommodateするには，



      ACCOM TEXT＼EXAMPLE1.MIZ

とします．accommodate では，環境部を読みこんで，その article で必要な，参照している article の定理，定義などを記号化したいくつかのファイルを作り，article の証明のチェックをする準備をします．ここで，エラーが出ることもあります．例えば，環境部に abstract file のファイル名を誤って書いてしまった場合などです．

accommodate は，毎回実行する必要はありませんが，環境部を変更したときは accommodate しなおさなければなりません．

7.4.2 Mizar チェッカー

これが通ったら，次に Mizar チェッカーを実行します．Mizar チェッカーを実行するには，



       MIZAR TEXT＼EXAMPLE1.MIZ

とします．すると，画面に表がでてきて，Parser，Analyzer，Checkerの順で，article をチェックし，チェックしている行数と，エラーの個数が表示されます．エラーが一つもなければ，Mizar のチェッカーに通ったことになります．



                                 PC Mizar Version 4.09


                                 Copyright (c) 1990,93 Mizar society



   Implimented by



      Andzrej Trybulec



      Czeslaw Bylinski

TEXT＼YA2.MIZ

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

図 7.1: Mizar 実行画面

7.4.3 エラーがある場合

エラーがある場合，ACCOM，MIZAR いずれのあとにも，ERRFLAG というコマンドを使って，エラー番号を，articleにコメントの形で記入します．



        ERRFLAG  TEXT＼EXAMPLE1.MIZ

とします ．いずれのコマンドも拡張子 .MIZ は省略することができます．

エラーメッセージを見るには，別のファイル（MIZAR.MSG）をエディターで 見る必要があります．

7.4.4 便利なコマンド

また，ACCOM と MIZAR をまとめた MIZ.BAT というバッチコマンドがあり，



       MIZ　TEXT＼EXAMPLE1.MIZ

とすることで，accommodate を実行し，さらに Mizarチェッカーを実行します．

さらに便利なバッチコマンドとして，MIZF.BAT があり，



       MIZF　TEXT＼EXAMPLE1.MIZ

とすると，accommodateする必要があるかをどうかを調べて，必要なときには accommodate を実行し，そのあと Mizar チェッカーを実行します．さらにエラーがある場合，エラー番号をコメントの形で article に書きこみ，article の最後には発生したエラー番号とエラーメッセージの対照表が書きこまれます (書きこまれたコメントは，次に MIZF コマンドを実行したときに取り除かれます．)．

7.4.5 エディターから Mizar を呼び出す方法

また，専用のマクロを利用し，Multi Editor から Mizarチェッカーを呼びだすことができます．Multi Editorで，ALT + F5とすると，Mizar チェッカーを呼びだして実行します．この場合，errflag は実行しませんので，article の中にエラー番号はコメントの形では入りませんが，テンキーの + キーと - キーを使うことにより，エラーのショートメッセージが画面の左上に表示されます．+ キーを押すことにより，次のエラーを表示し，逆に - キーを押すと１つ前のエラーを表示します．エラーがない場合

No more errors

と表示されます．ただし，この機能を使用するためには，SHORT.MSG というファイルをロードしておかなければいけません．

エラー番号と，エラーメッセージの対照表は，ディレクトリ MIZAR の下の MIZAR.MSG というファイルに，次のような形式で入っています．

# 1

It is not true

# 4

This inference is not accepted

# 9

Too many instantiations

SHORT.MSG は，エラーメッセージが MIZAR.MSG よりも短く書いてあるものです．

通常，Mizar article を書くときは，頻繁に Mizar チェックをしながらエラーを１つ１つ取っていくという作業になりますので，Multi Editor を利用することにより，効率よく，Mizar article を書くことが出来ます．

なお，Multi Editor用の Mizar専用マクロについては，著者までお問いあわせください．