A Practical Guide To Mizar/Installation

The Mizar system and the Mizar Mathematical Library are publicly available for download and may be used by anyone free of charge for non commercial purposes. The contents of the Mizar distribution is copyrighted by the Association of Mizar Users which maintains the Mizar Mathematical Library and coordinates the development of Mizar software.

—Adam Grabowski et al., Mizar in a Nutshell

Download the package or executable for your system from the official download page. It is recommended to get the package/executable under "More releases" because that one is most likely more up to date.

On Windows

The executable extracts a few files into the directory it is located in, so maybe create a temporary folder to execute it in. Then open a command line or power shell in that directory and execute INSTALL C:\mizar (you can change the target directory of course).

Afterwards you must set an environment variable MIZFILES to the target directory you just chose. It is also recommended to add the target directory to your PATH variable.

On Linux

Unpack the package into a temporary folder and call ./install.sh from your shell of choice. You will be asked where to copy the files to.

Afterwards you must set an environment variable MIZFILES to the folder with the shared files you just chose. Similarly it is your responsibility that the Mizar executables are on your PATH.

Editor

You will need a plain text editor of some kind (not Word) to write your Mizar articles in. On Windows you can use Notepad or install Notepad++. On Linux, you should have a plain text editor delivered with your distribution.

Some people also use Vim or Emacs or IDEs at their text editor. All valid choices.

Testing your Installation

Designate a directory for your own Mizar articles. Don't use the directory where Mizar had been installed, as that one gets overwritten when you update Mizar (by installing a newer version over it) and you might loose your files.

For the rest of this book it will be assumed that you are in a folder named TEST (located in your Mizar article folder) with your console/shell. Create subfolders named text and dict, and in text create a new file named test.miz and fill it with the following:

environ
begin

That's the "Hello World" of Mizar. Now when you execute the command mizf text/test (still from within the TEST folder) you should get output like this:

Make Environment, Mizar Ver. 8.1.14 (Linux/FPC)
Copyright (c) 1990-2023 Association of Mizar Users

-Vocabularies  [   1]
-Constructors  [   1]
-Requirements  [   1]
-Registrations [   1]
-Notations     [   1]

Verifier based on More Strict Mizar Processor, Mizar Ver. 8.1.14 (Linux/FPC)
Copyright (c) 1990-2023 Association of Mizar Users
Processing: text/test.miz

Parser   [   2]   0:00
MSM      [   2]   0:00
Analyzer   0:00
Checker  [   1]
Time of mizaring: 0:00