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
How to run Athena | Coq | Isabelle codes remotely?
370 views Asked by Mehmet Taha Meral At
1
There are 1 answers
Related Questions in COMPUTER-SCIENCE
- Add additional fields to Linq group by
- couldn't copy pdb file to another directory while consuming wcf web service
- Why are the aliases for string and object in lowercase?
- WPF MessageBox Cancel checkbox check
- Resolve object using DI container with object instance
- Creating a parametrized field name for a SELECT clause
- Does compiler optimize operation on const variable and literal const number?
- Get data from one form to another form in C#
- Writing/Overwriting to specific XML file from ASP.NET code behind
- Deleting Orphans with Fluent NHibernate
Related Questions in BACKGROUND-PROCESS
- Add additional fields to Linq group by
- couldn't copy pdb file to another directory while consuming wcf web service
- Why are the aliases for string and object in lowercase?
- WPF MessageBox Cancel checkbox check
- Resolve object using DI container with object instance
- Creating a parametrized field name for a SELECT clause
- Does compiler optimize operation on const variable and literal const number?
- Get data from one form to another form in C#
- Writing/Overwriting to specific XML file from ASP.NET code behind
- Deleting Orphans with Fluent NHibernate
Related Questions in COQ
- Add additional fields to Linq group by
- couldn't copy pdb file to another directory while consuming wcf web service
- Why are the aliases for string and object in lowercase?
- WPF MessageBox Cancel checkbox check
- Resolve object using DI container with object instance
- Creating a parametrized field name for a SELECT clause
- Does compiler optimize operation on const variable and literal const number?
- Get data from one form to another form in C#
- Writing/Overwriting to specific XML file from ASP.NET code behind
- Deleting Orphans with Fluent NHibernate
Related Questions in ISABELLE
- Add additional fields to Linq group by
- couldn't copy pdb file to another directory while consuming wcf web service
- Why are the aliases for string and object in lowercase?
- WPF MessageBox Cancel checkbox check
- Resolve object using DI container with object instance
- Creating a parametrized field name for a SELECT clause
- Does compiler optimize operation on const variable and literal const number?
- Get data from one form to another form in C#
- Writing/Overwriting to specific XML file from ASP.NET code behind
- Deleting Orphans with Fluent NHibernate
Popular Questions
- How do I undo the most recent local commits in Git?
- How can I remove a specific item from an array in JavaScript?
- How do I delete a Git branch locally and remotely?
- Find all files containing a specific text (string) on Linux?
- How do I revert a Git repository to a previous commit?
- How do I create an HTML button that acts like a link?
- How do I check out a remote Git branch?
- How do I force "git pull" to overwrite local files?
- How do I list all files of a directory?
- How to check whether a string contains a substring in JavaScript?
- How do I redirect to another webpage?
- How can I iterate over rows in a Pandas DataFrame?
- How do I convert a String to an int in Java?
- Does Python have a string 'contains' substring method?
- How do I check if a string contains a specific word?
Popular Tags
Trending Questions
- UIImageView Frame Doesn't Reflect Constraints
- Is it possible to use adb commands to click on a view by finding its ID?
- How to create a new web character symbol recognizable by html/javascript?
- Why isn't my CSS3 animation smooth in Google Chrome (but very smooth on other browsers)?
- Heap Gives Page Fault
- Connect ffmpeg to Visual Studio 2008
- Both Object- and ValueAnimator jumps when Duration is set above API LvL 24
- How to avoid default initialization of objects in std::vector?
- second argument of the command line arguments in a format other than char** argv or char* argv[]
- How to improve efficiency of algorithm which generates next lexicographic permutation?
- Navigating to the another actvity app getting crash in android
- How to read the particular message format in android and store in sqlite database?
- Resetting inventory status after order is cancelled
- Efficiently compute powers of X in SSE/AVX
- Insert into an external database using ajax and php : POST 500 (Internal Server Error)
I can only give an partial answer for Isabelle:
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, ...
There are also other IDEs like Isabelle/Eclipse and Clide (web-based). For your use case, Clide appears to be highly relevant.
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.
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.