如何在 Windows 10 上将 MMT 注册为 Isabelle 组件调用 isabelle mmt_build？

编程问答 2022-05-17

问题描述

我在 C:\Homes\Isabelle2021\Isabelle2021 中安装了 Isabelle2021，在 C:\Homes\MMT21 中安装了 MMT（来自 https://uniformal.github.io//doc/setup/），并且我在 C:\Homes\Isabelle2021\Isabelle2021\ 中添加了其他条目etc\Components 文件：

/cygdrive/c/Homes/MMT21
/cygdrive/c/Homes/MMT21/systems/MMT/deploy

但是我的 cygwin-terminal.bat 命令给出了找不到组件的错误：

C:\Homes\Isabelle2021\Isabelle2021>cygwin-terminal
This is the GNU Bash interpreter of Cygwin.
Use command "isabelle" to invoke Isabelle tools.

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle mmt_build
*** UnkNown Isabelle tool: "mmt_build"

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021

我已尝试关注https://drops.dagstuhl.de/opus/volltexte/2020/13065/pdf/LIPIcs-TYPES-2019-1.pdf：

如果 Mmt 目录作为组件注册到 Isabelle，它 提供了一个工具 isabelle mmt_build (shell script) 来构建 MMT 伊莎贝尔支持已启用。由此产生的 mmt.jar 将提供进一步 工具 isabelle mmt_import 和 isabelle mmt_server（在 Scala 中）到 执行导入并查看其结果。用户只需要调用， 例如，伊莎贝尔 mmt_import -B ZF。

我的努力有什么问题？ Isabelle 组件的注册是否需要额外的活动？ mmt.jar 真的如此适应 Isabelle（一种与 MMT 是非常通用的系统相反的特定工具），以至于 mmt.jar 真的包含这样的 mmt_build 命令？

我将阅读 https://isabelle.in.tum.de/dist/Isabelle2021/doc/system.pdf 第 7.2 章“管理 Isabelle 组件”，也许它会有所帮助，也许它适用于 Windows...

解决方法

这是部分答案。由于错误消息，无法简单添加 MMT 目录：

tomr@ /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle components -x /cygdrive/c/Homes/MMT21
*** Bad component directory: "/cygdrive/c/Homes/MMT21"

我在 Isabelle 源代码 https://isabelle-dev.sketis.net/file/data/ldiwqhsxa4d5zojczqye/PHID-FILE-2yuwbxlojqunqpdcqvqg/file 中找到了原因：

def update_components(add: Boolean,path0: Path,progress: Progress = new Progress): Unit =
   {
     val path = path0.expand.absolute
     if (!(path + Path.explode("etc/settings")).is_file &&
         !(path + Path.explode("etc/components")).is_file) error("Bad component directory: " + path)

因此，MMT 目录必须包含 etc/settings 文件（对于用作 Isabelle 组件的目录）。 MMT 没有，所以，我从现有的 Isabelle 组件中抓取了一个这样的文件，并将其修改为：

# -*- shell-script -*- :mode=shellscript:

classpath "C:/Homes/MMT21/mmt.jar"

isabelle_scala_service "isabelle.FlatLightLaf"
isabelle_scala_service "isabelle.FlatDarkLaf"

在 MMT21 目录中有该文件后，我设法将 MMT21 添加为组件：

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle components -u /cygdrive/c/Homes/MMT21
Added component "/cygdrive/c/Homes/MMT21"

但是，不幸的是，它没有解决我最初的问题，我仍然收到一个错误：

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle mmt_build
*** Unknown Isabelle tool: "mmt_build"

所以，知道我将深入 Google 和各个项目站点以挖掘这个问题...

添加： 关于这个有很好的材料https://sketis.net/2019/mmt-as-component-for-isabelle2019和https://github.com/UniFormal/MMT/tree/master/src/mmt-isabelle，所以，看起来，有一个特殊的jar，而不是主要的mmt.jar。我现在正在阅读有关此内容的信息。我会看看它是否适用于 Isabelle2021，还是应该与我的旧 Isabelle2020 一起使用。

isabellemmt