как запустить Mizar на Mac - PullRequest
Новая
       28

как запустить Mizar на Mac

3 голосов
/ 25 июня 2019

Если это не правильный сайт обмена стека для этого типа вопроса, пожалуйста, дайте мне знать, где было бы более подходящим. Также дайте мне знать, если есть более подходящие теги для этого вопроса, и я добавлю их (или, если вы хотите / можете, добавьте их самостоятельно). Также я нахожусь на Mac в случае, если это уместно.

Я пытаюсь использовать Mizar. Я скачал его и сейчас пытаюсь следовать этому уроку: https://www.cs.ru.nl/~freek/mizar/mizman.ps.gz (вы можете найти этот урок в Интернете, если поискать статью «Написание Mizar за девять простых шагов» и перейти по первой ссылке).

Я пытаюсь выполнить команду mizf text / my_mizar.miz в соответствии с рекомендациями руководства на стр. 3 (верхняя середина страницы). Кажется, проблема в том, что мне не хватает файла mml.ini, я не уверен, куда поместить этот файл.

Я попытался поместить его в верхний каталог (например, в /), но это не сработало (также требовалось, чтобы я получил права root, что я бы предпочел не делать). Вот копия моей консоли, чтобы дать вам представление о том, что я сделал. 

➜  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

1 Ответ

0 голосов
/ 30 июня 2019

К счастью для вас mizf это не исполняемый файл, а bash скрипт.Так что если вы загляните внутрь него 

#!/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

Как видите, все файлы ищутся в каталоге в MIZFILES переменная 

$ ./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
...