如何运行雅典娜辅酶Isabelle远程编码? [英] How to run Athena | Coq | Isabelle codes remotely?

问题描述

我一直在创建Web IDE(WIDE)，用于在计算机科学中证明定理.您可能知道，有3种最常见的证明助手，分别是Athena，Isabelle和Coq.大多数计算机科学家可能会忘记他们的语法，范围等.我的Web IDE可以使用拖放设计和示例.您可以在其上编辑和编写其他代码，可以下载，共享，保存等.它也具有自己的解析器.到目前为止，一切都还可以.小心！这是我的问题:如何运行用户代码并获得结果(尤其是对于Athena http://proofcentral.org/)，当用户希望在我的Web IDE上运行其代码时.实际上，我可以通过mouse_event(user32)和其他带有pinvoke(平台调用)的控件来实现.我的程序通过Web将代码发送到正在运行的PC(不是服务器.由于服务器没有显示屏幕，所以程序不会知道单击到何处)，然后PC会获得代码.然后程序单击"emacs"图标.几秒钟后(用于打开和上传Athena的dll)，该程序将Athena的代码粘贴到emacs shell中. Emacs运行该代码并返回结果.之后，选择程序，将结果复制并返回到Web IDE.但是，这是一种怪异而棘手的方法.我想做最好的方法. 感谢您的关注.最好的

I' ve been creating a Web IDE (WIDE) for theorem proving in Computer Science. You may know, there are 3 most common proof assitants which names Athena, Isabelle and Coq. Most of computer scientist might forget their syntax, scopes etc. My Web IDE works with drag and drop desing and examples. You can edit and write additional code on it, you can download it, you can share it, you can save it etc. It has also own parser. So far everything is OK. Watch out! Here is my question: How can I run the users' codes and get the result (especially for Athena http://proofcentral.org/) when user would like to run their code on my Web IDE. Actually, I can do this via mouse_event (user32) and other ones with pinvoke(platform invoke). My program sends the codes via Web to running PC(not server. Because server hasn't screen, so program won't know click to where), then the PC get the codes. Then the program click to "emacs" icon. After a few seconds(for openning and uploading dlls of Athena), the program paste that Athena codes into emacs shell. Emacs run that codes and return the result. After that the program select, copy and return the result to Web IDE. However this is a freaky and tricky way. I would like to do best way. Thanks for your attention. Best

推荐答案

我只能为 Isabelle 提供部分答案:

I can only give an partial answer for Isabelle:

Isabelle本身是在Standard ML中实现的，但是为了与外部世界通信，它使用了称为 PIDE (= Prover IDE )的协议. PIDE的参考实现与Isabelle捆绑在一起并用Scala编写，因此可以与任何JVM语言一起使用. PIDE的主要应用是 Isabelle/jEdit ，它使用jEdit编辑器为Isabelle构建IDE，包括标记，连续检查，...

Isabelle itself is implemented in Standard ML, but for communicating with the external world, it uses a protocol called PIDE (= Prover IDE). The reference implementation of PIDE is bundled with Isabelle and written in Scala, so it can be used with any JVM language. The primary application of PIDE is Isabelle/jEdit, which uses the jEdit editor to build an IDE for Isabelle, including markup, continuous checking, ...

还有其他IDE，例如 Isabelle/Eclipse 和 幻灯片 (基于网络).对于您的用例，Clide似乎非常相关.

There are also other IDEs like Isabelle/Eclipse and Clide (web-based). For your use case, Clide appears to be highly relevant.

如果您想了解有关PIDE内部工作的更多信息，可以查阅Wenzel的相关论文，例如

If you want to know more about the inner workings of PIDE, you can consult the relevant papers by Wenzel, for example Asynchronous User Interaction and Tool Integration in Isabelle/PIDE and Isabelle as Document-oriented Proof Assistant.

现在终于有了无耻的插件:由于不时出现如何与Isabelle作为外部程序进行交互的问题，因此我将PIDE与一些其他实用程序打包为

Now, finally, shameless plug: Since the question of how to interact with Isabelle as an external program comes up every now and then, I've packaged PIDE with some additional utilities as libisabelle. It includes an example of a very simple ping/pong interaction with the prover.

这篇关于如何运行雅典娜辅酶Isabelle远程编码?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！