andriusvelykis / isabelle-eclipse

Eclipse integration for Isabelle proof assistant.
http://andriusvelykis.github.io/isabelle-eclipse
Eclipse Public License 1.0
12 stars 4 forks source link

Provide convenient API to check proof script #62

Open andriusvelykis opened 11 years ago

andriusvelykis commented 11 years ago

Some of requests from Isabelle/Eclipse users were to allow automatically check Isabelle proof scripts from within Eclipse applications. This use case is not for using the editor and prover IDE, but rather to integrate with Isabelle to check proof scripts automatically.

Provide a convenient API to do this: it should allow to check a given proof script and report whether there are any errors. This would likely involve some support around asynchronous execution.

Also this would possibly need an option to auto-start Isabelle without user interaction.