4

如果这不是此类问题的正确堆栈交换站点，请让我知道哪里更合适。也让我知道这个问题是否有更好的标签，我会添加它们（或者如果你想要/可以，自己添加它们）。如果相关的话，我也在Mac上。

我正在尝试使用 mizar。我已经下载了它，现在正在尝试遵循本教程：https ://www.cs.ru.nl/~freek/mizar/mizman.ps.gz （您可以通过谷歌搜索“在中编写 Mizar 文章”在线找到本教程九个简单的步骤'并按照第一个链接）。

我正在尝试按照第 3 页（页面中上部）教程推荐的命令 mizf text/my_mizar.miz。问题似乎是我缺少一个名为 mml.ini 的文件，我不确定将这个文件放在哪里。

我已经尝试将它放在顶层目录中（例如，在 / 中），但这不起作用（它还要求我 sudo 到 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
4

2 回答 2

1

可能的原因是未定义的 MIZFILES 变量。如果您以默认模式安装 Mizar System，则共享文件的默认路径（在 macOS 和 GNU/Linux 中）为/usr/local/share/mizar. 在使用系统之前运行export MIZFILES='/usr/local/share/mizar'，或者将其粘贴到 bashrc。即使对于默认设置也需要此变量是呃...次优选择。

有关更多信息，请查看macOS 安装自述文件。

于 2020-01-04T09:23:51.357 回答
0

幸运的是，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
于 2019-06-30T07:38:19.070 回答