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?
421 Views Asked by Mehmet Taha Meral At
1
There are 1 best solutions below
Related Questions in COMPUTER-SCIENCE
- 2D array - making it "torus" like
- How to get samples of different paths?
- How do I keep track of path in TSP?
- Need workaround to treat float values as tuples when updating "list" of float values
- How does a loop work at the lowest level
- Solving a complex recurrence relation for the Traveling Salesman
- Would this function be O(n^2log_2(n))?
- Watermark in a textbox c#/cs/aspx
- Writing a Recurrence Equation
- How to run Athena | Coq | Isabelle codes remotely?
- Computer Architecture/Assembly, Amdahl's Law
- Why is it that some user defined C++ functions won't work with big numbers?
- Quicksort Q: Finitely many distinct keys
- Computer architecture - How to find the addresses in a block
- Table seating, what algorithm to use?
Related Questions in BACKGROUND-PROCESS
- Move python code to background after running a part of it
- Efficient way of organizaing mail sending from Rails app
- Is it possible to create a long running process in NodeJs
- Background task spontaneous completion C#
- Rails ActiveJob and SSE: How to Update Page When An API Call is Finished
- How can I trigger an event only when the power button is pressed in iOS?
- How to develop an iOS app that notifies you even when turned off
- Get an accelerometer's device id(or monitor an accelerometer in the backbround) on WinRT
- How to fire a local notification in backround mode?
- WPF 4.5: How to create child thread and continue task to UI main thread?
- Running background process in c++ using pthread
- Errors executing jobs with background job manager gem called Que
- angularjs background process for sending data from db and deleting this data from db
- Background processes in Node.js
- How to run Athena | Coq | Isabelle codes remotely?
Related Questions in COQ
- CoqIDE loadpath error for ssreflect
- How to assign a natural number to variable in Coq?
- Handling let in hypothesis
- Sum of exponents with same base
- How to run Athena | Coq | Isabelle codes remotely?
- Is equality decidable on any coinductive type?
- Coq "convoy pattern"
- In coq, how to do "induction n eqn: Hn" in a way that doesn't mess up the inductive hypothesis?
- Pattern matching multiple constructors in a single clause in Coq
- How to use Coq GenericMinMax to prove facts about the reals
- what does the colon greater than sign mean in coq
- Subtyping in Coq
- How to write coq definitions with "subtypes"
- Stronger completeness axiom for real numbers in Coq
- When is the first input to `list_rec` not a constant function?
Related Questions in ISABELLE
- Using type classes to overload notation for constructors (now a namespace issue)
- Existing constants (e.g. constructors) in type class instantiations
- Automated tools for applying formal methods to verify security policy in existing software
- How to use a main bib file with the Isabelle document preparation system?
- Isabelle: Unsupported recursive occurrence of a datatype via type constructor "Set.set"
- How to run Athena | Coq | Isabelle codes remotely?
- Usage of "also have...finally have" in Isabelle
- Why won't the 'linordered_field_class.frac_le' rule work? (Isabelle)
- Limit of c^n (with ¦c¦<1) is 0 (Isabelle)
- 'real_of_int' and 'real' in Isabelle?
- Is there a lemma like "∃x. a^x = b" proved in Isabelle?
- Proof by induction with three base cases (Isabelle)
- Constraining type variables in locales
- Lists and simplification rules: More difficult when using @ rather than #?
- How type casting is possible in isabelle
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)
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?
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.