All done! After spending quite some time on writing the thesis, I have successfully completed my PhD studies in June 2015. The thesis, a lengthy 386 pages of PDF, contains a lot of ideas, descriptions and justifications on capturing interactive proof process to facilitate extraction of reusable proof strategies as well as for other uses.
The thesis is titled Capturing Proof Process and is available in the publications list. The tools described in this thesis — the ProofProcess framework — are available on GitHub. Time permitting, I am hoping to continue improving the tools and update them to the most recent versions of the supported theorem provers.
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.