Mizar System
Overview
The Mizar System is the only implementation of the
Mizar Language.
Originally, the Mizar system was implemented on an IBM-PC x86
compatibles under MS DOS. Now we distribute releases for
MS Windows, Intel-based Linux, Solaris and FreeBSD, and also Darwin/Mac OS X and Linux on PowerPC.
The whole Mizar system (including verifier) is coded in Pascal using
the Free Pascal compiler.
Andrzej Trybulec
is the author of the Mizar Language,
he is also the head of the team implementing the verifier:
- Grzegorz Bancerek
- Czeslaw Bylinski
- Adam Grabowski
- Artur Kornilowicz
- Robert Milewski
- Adam Naumowicz
- Andrzej Trybulec
- Josef Urban
Preparing a Mizar article
The mechanics of preparing a
Mizar Article
is as follows:
- The source text is prepared using any ASCII editor and typically
includes from 1500 to 5000 lines.
- The text is run through the
Accommodator.
The directives from the
Environment Declaration
guide the production of the
environment specific for the article. The environment is
produced from the available data base.
- Now the
Verifier
is ready to start checking.
The output contains remarks on unaccepted fragments of the source text.
These three steps are repeated in a loop until no errors are flagged
and the author is satisfied with the resulting text. Usually,
Accommodator and
Verifier are called within
mizf (or mizf.bat) user script.
Alternatively, Josef Urban's
Emacs-lisp Mizar mode
(now included in all Mizar distributions)
provides a fully functional interface to the Mizar System.
When finished, an article is submitted to the
Library Committee of Association of Mizar Users
for inclusion into the
Mizar Mathematical Library.
The contributed article is subject to a review and if needed
the authors must revise their file.
The contents of an accepted article is extracted by the
Exporter utility and incorporated
into the public data base distributed to all Mizar users.
- To summarize, Mizar System is based on three
programs named:
Accommodator,
Verifier,
Exporter.
Distribution
The distribution of the Mizar system and the
Mizar Mathematical Library
is free of charge for non commercial purposes.
NOTE: Almost all material contained in the Mizar distribution
is copyrighted.
Mizar Users Group
Lasek Brzozowy 15/9
02-792 Warsaw
POLAND
Downloads:
Latest Mizar releases (version 7.11.03, MML 4.128.1063)
for Win32, Linux (i386), Solaris (i386), FreeBSD (i386), Darwin/Mac OS X (i386), Darwin/Mac OS X (PPC), Linux (PPC) and Linux (ARM):
-
ftp://mizar.uwb.edu.pl/pub/system/current/
- Download via HTTP
Win32 releases:
-
ftp://mizar.uwb.edu.pl/pub/system/i386-win32/
Linux (i386) releases:
-
ftp://mizar.uwb.edu.pl/pub/system/i386-linux/
Solaris (i386) releases:
-
ftp://mizar.uwb.edu.pl/pub/system/i386-solaris/
FreeBSD (i386) releases:
-
ftp://mizar.uwb.edu.pl/pub/system/i386-freebsd/
Darwin/Mac OS X (i386) releases:
-
ftp://mizar.uwb.edu.pl/pub/system/i386-darwin/
Darwin/Mac OS X (PPC) releases:
-
ftp://mizar.uwb.edu.pl/pub/system/ppc-darwin/
Linux (PPC) releases:
-
ftp://mizar.uwb.edu.pl/pub/system/ppc-linux/
Linux (ARM) releases:
-
ftp://mizar.uwb.edu.pl/pub/system/arm-linux/
The file
readme.txt contains
instructions for installing Mizar on Win32. Similarly,
there are files
README for Linux (i386),
README for Solaris (i386),
README for FreeBSD (i386),
README for Darwin (i386),
README for Darwin (PPC),
README for Linux (PPC), and
README for Linux (ARM).
Other FTP sites
- Poland:
- ftp://ftp.mizar.org/
- Japan:
- ftp://markun.cs.shinshu-u.ac.jp/pub/mizar/
Home |
Project |
Language |
System |
Library |
JFM
Last modified: September 18, 2009