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 (1941-2013)
Josef Urban

Preparing a Mizar article

The mechanics of preparing a Mizar Article is as follows:

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 Mizar Mathematical Library is distributed under the the GPL and/or the CC-BY-SA license. The distribution of the Mizar system is freely available for download for any non commercial purposes.

NOTE: Almost all material contained in the Mizar distribution is copyrighted by the Association of Mizar Users (SUM). The source code of the Mizar verifier and accompanying tools is available to the members of SUM.

Downloads:

Latest Mizar releases (version 8.1.05, MML 5.37.1275) 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 | People | MML | FM | SUM ]

Last modified: August 15, 2016