[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

  http://www-pu.informatik.uni-tuebingen.de/i3p

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
  well-known environment.

* 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
  commands.

* 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.

Enjoy,

  Holger






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.