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]
-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

In most cases, only the 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

Technical Details

For proper work, Accommodator requires a correctly set environment variable MIZFILES. It must contain the path to the root of Mizar data base (usually 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).
[ Home | Project | Language | System | People | MML | FM | SUM ]

Last modified: April 9, 2010