I am pleased to announce the first official release of Isabelle/Eclipse! Some documentation has finally caught up with the code, some new shiny features have been added, a brand new website has surfaced, and Isabelle/Eclipse got its first stable release.
Isabelle/Eclipse provides an Eclipse integration for Isabelle proof assistant, based on Isabelle/Scala framework. It started as a port of Isabelle/jEdit to integrate with Eclipse IDE. Today Isabelle/Eclipse is available as a standalone prover IDE, as well as plug-ins for integration with Eclipse IDE of your choice.
Learn more about Isabelle/Eclipse and download it from its website:
Isabelle/Eclipse provides a prover IDE to use Isabelle theorem prover. The integration uses common Eclipse components to provide theory editing, mathematical symbols, completion assistance, cross-referencing, prover output and other features. By building on Eclipse it inherits various IDE goodies out of the box. Learn more about Isabelle/Eclipse features on the website. Also, check out the list of closed issues to see what has been implemented and fixed in this release.
Before you start Isabelle/Eclipse, I advise reading the Getting started page on the website. Also make sure you are using Java 7 and Isabelle 2013.
Reporting issues & contributing
Note that Isabelle/Eclipse still has several known issues, notably no support for sub/super-script, bold and other control symbols, as well as lack of nice UI to configure certain Isabelle options. You can view all open issues for Isabelle/Eclipse in the GitHub tracker.
Please report any bugs, feature requests, questions and other issues you encounter—I will appreciate your input!
Isabelle/Eclipse is open-source and the source code is available on GitHub. I welcome all contributions and help—if you see an open issue that you want to hack at, feel free to!
Isabelle/Eclipse started as an attempt to get Isabelle working from within Eclipse IDE. There are a number of formal methods tools building on the Eclipse platform and I hope that Isabelle/Eclipse will be useful to integrate them with the Isabelle theorem prover.
Let me know what you think!