时间戳

首页 > 解决方案 > 如何查看所有活动的 Isabelle 会话？

isabelle - 如何查看所有活动的 Isabelle 会话？

问题描述

这个问题与我的另一个问题有关如何从 Windows 安装中导出 Isabelle 会话？. 如果我指出正确的会话名称，也许可以解决其他问题。

所以 - 我的问题是 - 如果 jEdit 用于编辑某些自定义理论文件，如何查看所有活动的 Isabelle 会话。

我可以调用 jEdit 插件“插件 - 伊莎贝尔 - 浏览会话信息”，我在左侧面板中获取树：

+ isabelle-session:
  - HOL

所以 - 我猜 - HOL 是父会话，但当前理论文件的具体会话是其他的，也许是默认的，也许是未命名的？

当我导出 HOL 会话时，当前的理论文件不在导出中。所以 - 我试图导出这个未命名的默认会话，但没有结果：

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test1 -x *:**  Unsorted
*** Undefined session(s): "Unsorted"

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle export -O /cygdrive/c/test1 -x *:**  isabelle-session
*** Undefined session(s): "isabelle-session"

所以 - 如果我能看到所有活动的会话，包括最具体、最低级别的会话的名称（在其中直接处理当前的理论文件），那么我将能够导出这个具体的会话，因此 - 我的用于导入 mmt 的当前理论文件。

标签： isabelle

解决方案

出于文档目的， Isabelle mailing-list上也提出了这个问题。

基本上给出的答案是：

  1. 为您的新理论创建一个 ROOT 文件
  2. 确保 Isabelle 知道您的 ROOT 文件。通过使用 Isabelle 的选项“-d”或安装新会话（如 AFP）。

然后是类似的东西

$ isabelle export -d /path/to/my/ROOT/file -O /cygdrive/c/test -x *:** MySessionName

应该管用。

推荐阅读