时间戳

首页 > 解决方案 > 如何在 Windows 10 上将 MMT 注册为 Isabelle 组件（调用 isabelle mmt_build）？

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

问题描述

我已经在 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 脚本）来构建启用了 Isabelle 支持的 MMT。生成的 mmt.jar 将提供更多工具 isabelle mmt_import 和 isabelle mmt_server（在 Scala 中）来执行导入并查看其结果。用户只需要调用，例如，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 上运行......

标签： isabellemmt

解决方案

这是部分答案。由于错误消息，无法简单添加 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"

所以，知道我要深入到谷歌和各自的项目网站去挖掘这个......

补充：关于这个 有很好的材料https://sketis.net/2019/mmt-as-component-for-isabelle2019和https://github.com/UniFormal/MMT/tree/master/src/mmt-isabelle，因此，似乎有一个特殊的 jar，而不是主要的 mmt.jar。我现在正在阅读这个。我将看看它是否适用于 Isabelle2021，或者我应该将它与我的旧 Isabelle2020 一起使用。

推荐阅读