how to run mizar on mac

Question

If this is not the right stack exchange site for this type of question please let me know where would be more appropriate. Also let me know if there are better tags for this question and I'll add them (or if you want/can, add them yourself). Also I am on a mac in case that is relevant.

I am trying to use mizar. I have downloaded it and am now trying to follow this tutorial: https://www.cs.ru.nl/~freek/mizar/mizman.ps.gz (you can find this tutorial online by googling 'Writing a Mizar article in nine easy steps' and following the first link).

I am trying to the command mizf text/my_mizar.miz as recommended by the tutorial on page 3 (upper middle of the page). The problem seems to be that I lack a file called mml.ini, I am not sure where to put this file.

I have tried putting it in the top directory (eg, in /) but this didn't work (also it required that I sudo to root which I'd rather not do). Here is a copy of my console to give you a sense of what I have done.

➜  testing ls -R
dic     mml.ini text

./dic:
my_mizar.voc

./text:
my_mizar.err my_mizar.miz
➜  testing cat dic/my_mizar.voc
➜  testing cat text/my_mizar.miz
environ
begin
➜  testing mizf text/my_mizar.miz

**** File not found          ****
**** Can't open ' /mml.ini ' ****
➜  testing

Answer 1

Luckily for you mizf is not an executable but as bash script. So if you peek inside it

#!/bin/sh
#
#          Mizar Verifier, example shell command
#

accommodate()
{
 makeenv $1
 if [ "$?" = "0" ]
  then
   verify $1
  else
   errflag $1
   addfmsg $1 $MIZFILES/mizar
   exit 2
 fi
}

verify()
{
 verifier $1
 errflag $1
 addfmsg $1 $MIZFILES/mizar
}

if [ -z "$1" ]
 then 
  echo "> `basename $0` error : Missing parameter" 
  echo "Usage: `basename $0` mizar_article_name" 
  if [ -n "$MIZFILES" ]
   then 
    MizarReleaseNbr=`awk -F= '/MizarReleaseNbr/{print $2}' $MIZFILES/mml.ini`
    MizarVersionNbr=`awk -F= '/MizarVersionNbr/{print $2}' $MIZFILES/mml.ini`
    MizarVariantNbr=`awk -F= '/MizarVariantNbr/{print $2}' $MIZFILES/mml.ini`
    MMLVersion=`awk -F= '/MMLVersion/{print $2}' $MIZFILES/mml.ini`
    NumberOfArticles=`awk -F= '/NumberOfArticles/{print $2}' $MIZFILES/mml.ini`
    echo "MML ver. $MMLVersion.$NumberOfArticles for Mizar ver. $MizarReleaseNbr.$MizarVersionNbr.$MizarVariantNbr available in $MIZFILES"
  fi
  exit 1
 else 
  accommodate "`dirname $1`/`basename $1 .miz`"
fi

As you can see all every file is looked up in the directory in MIZFILES variable

$ ./bin/mizf my.miz

**** File not found          ****
**** Can't open ' /mml.ini ' ****

$ export MIZFILES=$PWD/share/mizar
$ ./bin/mizf my.miz
Make Environment, Mizar Ver. 8.1.09 (Darwin/FPC)
Copyright (c) 1990-2019 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.09 (Darwin/FPC)
Copyright (c) 1990-2019 Association of Mizar Users
Processing: ./my.miz

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

Answer 2

Possible cause is undefined MIZFILES variable. If you installed Mizar System in default mode, the default path for shared files (in macOS and GNU/Linux) is /usr/local/share/mizar. Just run export MIZFILES='/usr/local/share/mizar' before using the system, or paste this to bashrc. Requiring this variable even for default setup is uhm... suboptimal choice.

For more info check out macOS installation readme file.