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.
I have decided to dust off and finally release some projects that occupied some of my time in the past but then got forgotten or postponed somehow… The first of these is a new skin for Apache Maven site: Reflow Maven skin.
An obligatory screenshot follows. Read on for a bit more details about the skin.
Eclipse IDE can be extended by creating plug-ins that complement the existing IDE features. Furthermore, the plug-ins can be released as a standalone application (that may resemble Eclipse IDE) with custom branding and a streamlined selection of features, geared for a specific task. This is done by using the Eclipse Rich Client Platform (RCP) and the branding features available within it.
One of the most visible features of a standalone application is the application icon. Eclipse is a cross-platform application, however the application launchers for each operating system (OS) are native, thus they require different icons. In this post I tried to collect my notes on creating these different icons for different OS builds: their formats, and hints on producing them.
These instructions are for building a branded Eclipse product using Eclipse Tycho with Eclipse Juno (4.2) as the base platform. The experiences come from packaging a standalone IDE for developing Z formal specifications, which will be released as part of the latest Community Z Tools in the nearest future.
Z/EVES is an interactive theorem prover for Z notation. It can be used to develop Z specifications and reason about them. It has a number of attractive features, such as an easier learning curve (in comparison to related theorem provers, e.g. Isabelle), powerful proof tactics, and the ability to do proofs in Z notation.
Unfortunately, it is no longer being developed. Neither is it open sourced (as of the time of writing), so we have to make do with what we have: the last version (2.4.1 apparently) was released in 2005 for Windows, Linux and Solaris platforms. There is no Z/EVES runtime for Mac OS X, however, which is problematic knowing that Macs are not rare in academia..
Fortunately, I have managed to get the Windows version of Z/EVES running on Mac OS X using Wine. I could install Z/EVES on my OS X Lion to run both as command line (to integrate with CZT Eclipse!—see screenshot) as well as using its Python GUI. The (more) detailed instructions follow.
I will be attending (and talking at!) the Doctoral Symposium at FM2012 (18th International Symposium on Formal Methods) in Paris next week. A preprint of the accepted publication on my PhD research is available from here, as well as a Newcastle technical report.
The publication and talk uses the current working title of my PhD: Inferring the Proof Process. I try to cover the ideas of what I am aiming for with my research (i.e. what describes a proof process? how can we capture and understand the expert’s ideas?), as well as current results (the ProofProcess framework) and future directions (i.e. how can we automate the proof process capture and analysis?)
The actual abstract is below:
This PhD project aims to investigate how enough information can be collected from an interactive formal proof to capture an expert’s ideas as a high-level proof process. It would then serve for extracting proof strategies to facilitate proof automation. Ways of inferring this proof process automatically are explored; and a family of tools is developed to capture the different proof processes and their features.