如何查看所有活跃的 Isabelle 会话？

Question

这个问题与我的另一个问题有关How to export Isabelle session from the Windows installation?。如果我指出正确的会话名称，也许可以解决其他问题。

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

我可以调用 jEdit 插件 'Plugins - Isabelle - Browse Session information' 并在左侧面板中获取树：

+ 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。

Answer 1

出于文档目的，这个问题也在 Isabelle mailing-list 上被问到。

基本上给出的答案是：

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

然后是

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

应该可以。

Answer 2

isabelle build -a -n -v

是这个问题的准确答案。例如：

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle build -a -n -v
Started at Sat Mar 27 01:28:30 GMT+2 2021 (polyml-5.8.2_x86_64_32-windows on DESKTOP)
ISABELLE_TOOL_JAVA_OPTIONS="-Djava.awt.headless=true -Xms512m -Xmx4g -Xss16m"
ISABELLE_BUILD_OPTIONS=""

ML_PLATFORM="x86_64_32-windows"
ML_HOME="/cygdrive/c/Homes/Isabelle2021/Isabelle2021/contrib/polyml-test-f86ae3dc1686/x86_64_32-windows"
ML_SYSTEM="polyml-5.8.2"
ML_OPTIONS="--minheap 500"

Session Pure/Pure
Session CTT/CTT
Session Cube/Cube

虽然这个命令列出了所有的session，但是可以看到这个列表不包含当前打开的自定义理论文件。

Isabelle 演示文稿的最大问题是以下问题：新手急于开始创建新的理论文件，这就是他或她打开 jEdit、创建新文件、导入 parent 理论并开始的原因编辑。人们期望一切都会好起来的。但这不好。这种独立的理论文件可以编辑和检查，但它是孤立的，不属于任何sessions。例如。此文件没有自己的 session。此文件不属于 parent session（例如 HOL 或 Pure），因为文件未作为 parent sessions.

的一部分导出

因此 - 人们应该在 Isabelle 文档中清楚地记录人们最初应该创建 session（类似于工业编程语言的项目或解决方案 folder/file）。 session 的创建非常棘手且出人意料地令人困惑 - 应该创建 ROOT 文件，将其放在某个目录中，然后从命令行启动 jEdit，并使用特殊选项指示 jEdit 应加入此 folder/session .只有在这样的设置之后，当前编辑的文件才属于 session（我正在尝试检查此设置）。

每个 IDE（如 Visual Studio 或 Eclipse）都提供 IDE-in-build 用于管理 solution/project 基础设施的工具，所以 - 也许 jEdit 有这样的 session 管理插件，也许 jEdit 启动过程可以变得更直观，邀请明确使用 sessions，因为现代 IDEs 迫使用户将他们的所有工作放在解决方案或项目中。

例如我已经创建了 ROOT 文件（我希望它能工作。我还没有找到 one-simple-theory-file 项目的 ROOT 示例文件）：

chapter Algo

session Algo = Pure +
  description "
    Classical Higher-order Logic.
  "
  options [strict_facts]
  sessions Tools
  theories
    Main (global)
    Complex_Main (global)
  document_theories
    Tools.Code_Generator
  document_files
    "root.bib"
    "root.tex"

并且我尝试使用 - 启动 jEdit，但出现错误（请参阅跟踪）：

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle jedit -d /cygdrive/c/Workspace-Isabelle2021 -l Algo
01:58:55 [AWT-EventQueue-0] [error] PluginJAR: Error while starting plugin isabelle.jedit.Plugin
01:58:55 [AWT-EventQueue-0] [error] PluginJAR: *** Duplicate global theory "Main" (line 3 of "/cygdrive/c/Homes/Isabelle2021/Isabelle2021/src/HOL/ROOT")
01:58:55 [AWT-EventQueue-0] [error] PluginJAR:  at isabelle.Exn$ERROR$.apply(exn.scala:28)
01:58:55 [AWT-EventQueue-0] [error] PluginJAR:  at isabelle.Exn$.error(exn.scala:32)

经过一些实验，我将 ROOT 缩短为：

chapter Algo

session Algo = Pure +
  description "
    Classical Higher-order Logic.
  "
  options [strict_facts]
  document_files
    "Max_Of_Two_Integers_Real.thy"

我开始使用 jEdit：

tomr@DESKTOP /cygdrive/c/Homes/Isabelle2021/Isabelle2021
$ isabelle jedit -d /cygdrive/c/Workspace-Isabelle2021 -l Algo

但是有两件奇怪的事情：

Draft/scratch 文档空白页显示为默认文档。当我尝试加载我的理论文件 (Max_Of_Two_Integer_Real.thy) 时，jEdit 中没有任何内容会显示 Workspace-Isabelle2021 是我的默认目录 session.
我尝试再次导出 sessions - 但没有成功：

例如

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

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

这真是令人费解。我首先检查的是 Isabelle session 插件。我希望看到 session 算法，但有 session 未排序。但是 - 这些 session 中的 none 可以导出 - 如未定义的 session 消息所示。

如何查看所有活跃的 Isabelle 会话？

How to see all the active Isabelle sessions?

isabelle