我们如何使用 python 程序访问 Coq 或 Isabelle/HOL？

Question

我想使用我的 python 程序访问 Coq 或 Isabelle/HOL 交互式定理证明器。有没有 python 包可用？请推荐

Answer 1

我不是 Isabelle 方面的专家，但我相信最常用的界面是 IDE 使用的 Scala API，不幸的是，我不能说更多。

关于 Coq，多年来的标准交互方式一直是与终端 REPL 界面对话。那不是很方便。您有更新的 IDE protocol，但是我不建议对其进行大量投资，因为它很快就会进行重大修订，（希望对其进行改进 :)）

一个不成熟但可行的替代方案是 SerAPI，[免责声明我是作者]，它提供了协议中接下来会发生什么的一瞥。取决于您想做什么，它可能会起作用。不幸的是，没有 Python 绑定，因为我无法弄清楚如何最好地进行异步编程，但是欢迎 help/PRs。

最后，您当然可以直接使用 OCaml 从 Python 与 Coq 对话。同样，根据您的用例，它会很有趣或非常具有挑战性。

Answer 2

这是关于如何启动 Isabelle 实例并从 Python:

执行 RPC 调用的非常粗略的草稿

import $ivy.`info.hupel::libisabelle-setup:0.9.2`
import $ivy.`org.python:jython-standalone:2.7.1`

import javax.script.ScriptEngineManager

val python = """
  |from info.hupel.isabelle.api import Configuration, Version
  |from info.hupel.isabelle.japi import JResources, JSetup, JSystem, Operations
  |res = JResources.dumpIsabelleResources()
  |print res
  |config = Configuration.simple("Protocol")
  |print config
  |env = JSetup.makeEnvironment(JSetup.defaultSetup(Version.Stable("2016-1")), res)
  |print env
  |sys = JSystem.create(env, config)
  |print sys
  |response = sys.invoke(Operations.HELLO, "world")
  |print response
  |sys.dispose()""".stripMargin

new ScriptEngineManager().getEngineByName("python").eval(python)

这是用 Scala 代码包装的，原因很简单，因为这是让 Jython 工作的最简单方法。

要执行上面的脚本，请将其保存为文件（例如 isa.sc），为 Scala 下载 the Ammonite REPL，然后运行就像 ammonite isa.sc 一样。这应该需要一些时间来做一些设置，最后，应该会出现这样的东西：

info.hupel.isabelle.japi.JResources@59d0fac9
session Protocol
<Isabelle2016-1> at /home/lars/.local/share/libisabelle/setups/Isabelle2016-1
info.hupel.isabelle.japi.JSystem@138a952f
Hello world

这演示了来自 Python 的非常简单的 Isabelle 引导。

我们如何使用 python 程序访问 Coq 或 Isabelle/HOL？

How we can access Coq or Isabelle/HOL using python program?

python

coq

isabelle