isaplanner

Last updated: 2018-02-01 16:58:37 +0000

Upstream URL: git clone http://chriswarbo.net/git/isaplanner.git

Contents of README.md follows

IsaPlanner - a Proof Planner for Isabelle

IsaPlanner is a proof planner for Isabele. It facilitates the encoding of reasoning techniques and their application to prove theorems in Isabelle. In particular, it provides an inductive prover based on Rippling, as well as automatic theory formation tools (IsaCoSy and IsaScheme)

IsaPlanner is written in Isabelle/StandardML (based on PolyML

The old IsaPlanner homepage is here: http://dream.inf.ed.ac.uk/projects/isaplanner

See the INSTALL file for more information on how to install IsaPlanner. (briefly, run the command “isabelle make” and you are done)

You want to be familiar with Isabele before trying to use IsaPlanner. :)

This version of IsaPlanner is intended to work with Isabelle 2015 and requires that you have a clone/download of the Isabelle-2015 branch of isaplib in your Isabelle contrib directory.

Quickly playing with IsaPlanner

Simply open the file <code>quicktest.thy</code> in Isabelle 2015.

Setup IsaPlanner Heap

Change into the IsaPlanner directory.

<pre><code>cd IsaPlanner export ISAPLANNER_DIRECTORY=$(pwd)</code></pre>

To use IsaPlanner, you should build the heap from IsaPlanner dir by running the command:

<pre><code>isabelle build -d $ISAPLANNER_DIRECTORY -b HOL-IsaPlannerSession</code></pre>

where <code>ISAPLANNER_DIRECTORY</code> is dierctory containing IsaPlanner (optionally relative to the current directory), that was set above.

This will build and ML heap (also sometimes referred to as an Isabelle Session) called “HOL-IsaPlannerSession” containing Isabelle/HOL with IsaPlanner tools loaded in a theory “IsaP”. Now you can make a new theory that imports “IsaP” and in that theory you can use IsaPlanner and IsaCoSy.

For example, start Isabelle with the Isabelle session ‘HOL-IsaPlannerSession’ using this command:

<pre><code>isabelle jedit -l HOL-IsaPlannerSession -d $ISAPLANNER_DIRECTORY</code></pre>

Running tests

<pre><code>isabelle build -d $ISAPLANNER_DIRECTORY -b IsaPlanner-Test</code></pre>

Developing new techniques

You’ll be doing ML programming in Isabelle, so make sure to have the Isabelle CookBook handy.

TODO: complete this section. :)

Using the Docker environment

Build the IsaPlanner docker image:

<pre><code>docker build -t theorymine/isaplanner:2015.0.2 .</code></pre>

Start a new docker container from the image running a bash shell:

<pre><code>docker run -i -t theorymine/isaplanner:2015.0.2 /bin/bash</code></pre>