Tom*_*Tom 3 python coq isabelle
我想使用我的python程序访问Coq或Isabelle/HOL交互式定理证明器.有没有python包可用？请建议
我不是Isabelle的专家,但我相信最常用的界面是IDE使用的Scala API,遗憾的是,我不知道更多.
关于Coq,相当多年的标准交互方式一直在与终端REPL接口进行对话.那不是很方便.你有一个更新的IDE协议,但我不建议大量投资,因为它很快就会有一个重大修订,(希望改进它:))
一个非成熟但有效的替代方案是SerAPI,[免责声明我是作者],它提供了协议中接下来会发生什么的一瞥.根据您的想法,它可以工作.不幸的是,没有Python绑定,因为我无法弄清楚如何最好地进行异步编程,但欢迎帮助/ PR.
最后,您当然可以直接使用OCaml与Python的Coq交谈.同样,根据您的使用情况,它将是有趣的或非常具有挑战性的努力.