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?
424 views Asked by Mehmet Taha Meral At
1
There are 1 answers
Related Questions in COMPUTER-SCIENCE
- what's the difference between "nn layout" and "nt layout"
- Theory of Comp Sci - State Diagrams NFAs
- What is devops meaning ? What requirement?
- How to test that a specific sorting algorithm was actually implemented?
- Creating a more efficient algorithm for taking the third largest difference an element has with another element in the list in python
- Theory of computer science problems
- Choosing a sequence of bitwise operations
- How to determine the time complexity of a recursive function that has a loop enclosed in it?
- Find median in constant time O(1)
- The factorial of an inputted number in Flowgorithm
- How come checking for printable bytes is faster with the "in" operator rather than interval comparisons?
- PageRank Algorithm on a Graph with a Sink Node
- recursion relation problem solve only using back substitution method
- Integrating Jenkins CI/CD with WinDev Framework for Academic Project
- Formatting multiplication tables in python; not how to, just some explanation
Related Questions in BACKGROUND-PROCESS
- Run Jobs Sequentially, in the Background, in Bash
- Logging after return statement in method && asynchronous logging
- Handling Data Transmission in Foreground Service with WebSocket and Managing Downtime
- Is anyone used react-native-background-geolocation?
- How to properly request location permissions for background location updates in Flutter?
- Configure a background service in .NET 8 MAUI for Windows
- Run method works with widgets from background task in Flutter Dart
- Persistent Background Task in iOS 2024
- setWallpaper in Android after app terminated
- React-native-background-action Cannot read property 'start' of null
- How to Sync Data to Server from a Flutter Windows App Even When the App is Closed?
- Set wallpaper in Headless JS react native background task
- How to run a service in background on Android 10? Rooted device
- how can i make a php function to continue to run with the while loop in background?
- How to convert java application with process in background to installer?
Related Questions in COQ
- Coq : mutually recursive definitions with [mrec] in InteractionTrees Library
- Is there a function that returns a list of values with specific type in OCaml?
- How to prove (X !-> 3) =[ <{ X := X + 2 }> ]=> (X !-> 5)?
- Showing polynomial equality in coq/ssreflect
- Syntax of the case tactic in coq
- Why assuming singleton elimination and definitional proof irrelevance leads to UIP, in Coq?
- Understanding nat_ind2 in Logical Foundations
- What `dependent induction` tactic does in Coq and how to use it
- Split multiple conjuncts in the goal
- Coq can't define an inductive proposition
- Coq Decreasing Argument mapping
- The `specialize` tatic in Coq does not work well with typeclasses?
- Multiple Assignements in a Coq Map to the same value
- Decider for lists In Fixpoint
- VSCoq Error: Connection to server got closed. Server will not be restarted
Related Questions in ISABELLE
- Proof on inductive sets
- Isabelle/HOL: How to handle `let` and `if`?
- Exists irrational number: sqrt fails to refine pending goal
- Proof by reductio ad absurdum in Isabelle
- I have a problem in Isabelle related to 'Clash of types' that I am unable to solve. Could someone help me?
- Customized datatype
- How to improve a LH=RH chain proof
- Locale inheritance after interpretation
- How to verify C functions with array parameters using Isabelle
- Is it possible to define a context for syntax rules?
- stuck on a proof (modeling IMP language)
- Isabelle Server HOL-Library Build Failed
- Isabelle/HOL: Induction fails because the assumption about the inductive predicate is not the first assumption
- Complex set comprehension
- Sledgehammer output with vampire
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?
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.