Accommodator is a program that processes the Environment Declaration part of a Mizar Article and creates the environment for the Verifier based upon available data base.
accom [options] article-file-name [environment-name]
Options: -v Process vocabularies -f, -p Process vocabularies and formats -P Process vocabularies, formats, lists of theorems, and lists of schemes -e Process vocabularies, formats, constructors, signatures, clusters, and notations -h Process built-in constructors specially -l Allow for source lines longer than 80 characters -s Stop on first error
article-file-name parameter is
needed. Moreover, it is recommended to use makeenv
utility instead of direct calls to accom.
makeenv first checks the environment and processes the
accommodation only when the environment is modified and must be rebuilt.
Options for makeenv: -a Force accommodation -n Use a new method of accommodation (experimental, not recommended) -l Allow for source lines longer than 80 characters -s Stop on first error
c:\mizar on MS Windows and
/usr/local/share/mizar on UNIX).
During accommodation, information stored in a local data base (if any)
takes precedence over that from the main data base indicated by MIZFILES.
Local data base and local vocabularies are searched for in subdirectories
prel and dict respectively of the current
directory (from where Accommodator is invoked).
Last modified: April 9, 2010