在没有 GUI 的情况下与 Isabelle 交互

问题描述

我正在尝试实现 Isabelle/JEdit 的命令行版本，以便我可以

1. 在另一个 docker/机器中运行 Isabelle 服务器
2. 允许集成更多编辑器，如 Vim 或 Emacs
3. 允许自动化代理检查和编写证明。

从 this question 看来，似乎无法将 JEdit 与 Isabelle 进程分开。我还阅读了 Isabelle systems manual 并且手册在协议方面没有太多信息。例如

$ isabelle server # On another machine/terminal

$ isabelle client

help
OK ["cancel","echo","help","purge_theories","session_build","session_start","session_stop","shutdown","use_theories"]
session_start
ERROR {"kind":"error","message":"Bad argument for command 'session_start'","argument":""}

另一个提供此类功能的库是 scala-isabelle，但我不清楚它是否可以执行此类交互。

解决方法

这是一项重大任务。

官方工具

从编辑的角度来看，我认为最简单的答案是使用 LSP 协议。 Isabelle 已有服务器，因此您无需重新发明轮子。

也可以直接在 Isabelle/ML 或 Isabelle/scala 中编写工具，特别是如果您希望最终将您的工具包含在 Isabelle 中。这也避免了启动 Isabelle 和基础会话等的整个处理过程。

我相信 Isabelle 流程更上一层楼。它适用于会议和理论，而不适用于个人目标。

外部工具

• There seem to be an existing PG integration,but I have never tested it

免责声明：在我的空闲时间，I work on an LSP client for Isabelle for emacs，所以我倾向于相信它比PG更好。我之前通过 SSH 使用过 Isabelle。