[isabelle] Announcing I3P
Dear Isabelle users,
It is my pleasure to announce the first public release
of I3P, an Interactive Interface for the Isabelle Prover.
It is available from
The two goals of the I3P development are interactivity
and extensibility: users should be able to interact with
an interactive theorem prover in more ways than executing
and undoing commands, and they should be able to add
in well-defined ways specific user-interface functionality to
support them in their specific projects.
Here are a few reasons why you might want to give I3P a try:
* It offers the main functionality of the Emacs-based
ProofGeneral: as the main difference, the keyboard shortcuts
replace Ctrl-C by Ctrl-Shift.
* It builds on the Netbeans/Swing frameworks and thus offers
standard UI features: your students might appreciate the
* It handles copy & paste with XSymbols correctly.
* It is portable and has been used under Linux and MacOS.
(Windows/Cygwin support will be added shortly.)
* It is fast: the design pays specific attention to handling
large numbers of trace messages and large messages efficiently:
there is no real need to wait while the UI is scanning your traces.
* It offers command-local tracing: several posts to this list
have asked whether it is possible to turn on tracing for
single commands. I3P offers this capability (command-local options)
on the interface side, by having the prover driver issue option
changes before and after command execution.
* It has small release cycles: due to test-driven development of
the developed infrastructure layer (with the number of test
cases approaching 400), I feel confident in releasing updates
in short periods. An AutoUpdate-Service is included to inform
you about new versions.
* It is extensible: the existing modules provide general
and documented mechanisms for plugging in new views and
* It provides a framework for driving Isabelle-2009/-1:
several posts to this list have asked how to use Isabelle
as a background prover. The test cases of the Isabelle
driver of I3P show how to achieve this in a simple manner.
* The installation effort is minimal anyway: just download the
binary, unzip, and start i3p/bin/i3p.
At most, you may want to install the IsabelleMono.ttf from
Isabelle2009-1/lib/fonts on your system and choose it for the
display under Tool/Options/Fonts.
I would also like to thank Makarius Wenzel, Burkhart Wolff,
and Achim Brucker for discussions about the requirements
on user interfaces for Isabelle. Furthermore, they and
Alexander Krauss and Julia Trieflinger have courageously
agreed to act as beta-testers for I3P and have provided
invaluable feedback on shortcomings and usability issues.
I am very grateful for any feedback you might care to give.
This archive was generated by a fusion of
Pipermail (Mailman edition) and