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

Question

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

/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:

if the Mmt directory is registered to Isabelle as component, it provides a tool isabelle mmt_build (shell script) to build MMT with Isabelle support enabled. The resulting mmt.jar will provide further tools isabelle mmt_import and isabelle mmt_server (in Scala) to perform the import and view its results. Users merely need to invoke, e.g., isabelle 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...

有用

Answer 1

这是部分答案。由于错误消息，无法简单添加 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 and https://github.com/UniFormal/MMT/tree/master/src/mmt-isabelle，所以，看起来，有一个特殊的罐子，而不是主要的mmt.jar。我现在正在读这个。我会看看它是否适用于 Isabelle2021 还是应该与我的旧 Isabelle2020 一起使用。

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

How to register MMT as Isabelle component on Windows 10 (to call isabelle mmt_build)?

isabelle

mmt