Download, Install, Setup

Download/Install Isabelle

You need a recent version of Isabelle (Last tested with: Isabelle 2011-1). See the Isabelle Installation page for setting up Isabelle. Essentially, you have to uncompress the file, read the INSTALL text file and do what it says. You can ask me if you want some help on setting up multiple copies of Isabelle.

It is probably easier to use the official version, but you can also get a working version of Isabelle using mercurial with following command:

hg clone http://isabelle.in.tum.de/repos/isabelle

This will create a directory called isabelle. I don't know if recent snapshots are compatible with IsaPlanner - use at your own risk.

IsaPlanner from Subversion on sourceforge

To get a subversion checkout of IsaPlanner from sourceforge use the following command:

svn co https://isaplanner.svn.sourceforge.net/svnroot/isaplanner/trunk/IsaPlanner/IsaPlanner2011-1 IsaPlanner2011-1

This will create a directory called IsaPlanner2011-1, which contains all the IsaPlanner code, at the location you run the command.

Setup

Assuming Isabelle is installed correctly, you should be able to run the following command in the IsaPlanner2011-1 directory:

isabelle make

This will build the HOL_IsaP heap which sets up IsaPlanner and allows you to load Isabelle with the IsaPlanner libraries and tools.

Using IsaPlanner

At the moment we are re-figuring out how to make an interface to IsaPlanner without shell. To build on IsaPlanner, import the theory IsaP:

theory MyTheory
imports IsaP
begin
-- write your theory here --
end;

For some simple examples, see the file {{{IsaPlanner-2011/quicktest.thy}}}. Note that to use IsaPlanner's interactive tracer, you must look in the buffer *isabelle*. A proper manual and interface is in progress...

Writing your own code

Writing stuff for IsaPlanner generally involves writing Isabelle/ML code. Some very helpful information on this is provided by the Isabelle documentation project (The so-called Isabelle Cook-book).

Variations

With a development snapshot of PolyML

To use Isabelle/IsaPlanner with the cutting edge versions of PolyML, you can explicitly set this in Isabelle's settings file (either $HOME/.isabelle/etc/settings or $ISABELLE/etc/settings) with the line:

ML_SYSTEM=polyml-X.Y

where X.Y is the version number of PolyML.

If you have PolyML at a non-standard (for Isabelle) location, you will also need to set the ML_HOME variable to point to the directory where the PolyML executable is.