1

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

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

从这个问题来看，似乎没有办法将 JEdit 与 Isabelle 进程分开。我还阅读了 Isabelle系统手册，该手册在协议方面没有太多信息。例如

$ 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，但我不清楚它是否可以执行这种交互。

4

1 回答 1

4

这是一项重大事业。

官方工具

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

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

我相信伊莎贝尔流程更高。它适用于课程和理论，而不是个人目标。

外部工具

免责声明：在我的空闲时间，我为 Isabelle 为 emacs 开发 LSP 客户端，所以我倾向于相信它比 PG 更好。我之前通过 SSH 使用过 Isabelle。

于 2021-01-16T19:45:40.840 回答