Early release time!
I got around to creating proper build environments for all the code I have been working on. Using Eclipse Tycho I was able to create Maven build configurations for all the projects. Now producing Eclipse update sites for end-users is (mostly) a single-click process.
So finally I can offer easy install sites for Isabelle/Eclipse and the ProofProcess framework. I have also added an update site for CZT Eclipse plug-ins, which now feature integration with Z/EVES theorem prover.
Note that these are early technical preview releases. This means that we have been using the tools ourselves, but they still have rough edges and are likely to change. Also, the documentation is quite lacking—we hope to improve in all of these areas! So please report any problems/issues/suggestions you encounter.
Isabelle/Eclipse
Isabelle/Eclipse provides an Eclipse-based Prover IDE for Isabelle proof assistant, based on Isabelle/Scala framework. It started as a port of Isabelle/jEdit Prover IDE. To install the latest version, point your Eclipse IDE to this update site:
When installed, launch Isabelle as an external tool. Currently only Isabelle2012 is supported. Please report issues in the GitHub tracker.
ProofProcess framework
ProofProcess framework is the tool goal of my PhD. Currently its core is available. It aims to capture, store, analyse and display proof process data from Isabelle and Z/EVES provers in Eclipse-based interface. The current version is available from this update site:
The data capture should start automatically with Isabelle/Eclipse or Z/EVES theorem provers and there are views available to display it. Note that scalability has not been tested much yet.
CZT for Eclipse + Z/EVES integration
We have updated Eclipse plug-ins for Community Z Tools and added integration with Z/EVES theorem prover for verifying Z specifications. The functionality will be released as CZT 1.6, but until we get around to doing that, the ‘nightly’ release of the Eclipse plug-ins is available from this update site:
When installed, launch Z/EVES as an external tool. Note that you will need to use Wine to run Z/EVES on Mac OS X. Please report issues in the SourceForge tracker.
Hopefully these will allow you to get a taste of the tools. Please try them out and check back for updates here and on their respective web sites.