Isabelle/UTP

A verification toolbox for Isabelle/HOL based on Unifying Theories of Programming

View project on GitHub

Installation Overview

  • Install Isabelle 2018
  • Add the Isabelle2018/bin directory to your PATH variable
  • Ensure that you have TeX Live installed. You need at least the basic distribution and also texlive-generic-recommended. It is probably easiest to install all of TeX Live (texlive-full).
  • If you’re using Windows (and thus Cygwin), you will need to install the wget package as well
  • Download and extract Isabelle/UTP (zip / tar / GitHub)
  • Run bin/utp-jedit UTP from the UTP installation directory.
  • The build script will obtain dependencies from the Archive of Formal Proof (AFP).
  • Isabelle/UTP will now be built. This is only done once. You should get a window like this:

Isabelle/UTP building

  • Compilation may take a little time, so make some tea or coffee
  • When the window disappears, go to File > Open..., and try to load tutorial/utp_hello_world.thy and see if it works

Isabelle/UTP success

Details

Installation requires that you have already installed the latest version of Isabelle on your system from http://isabelle.in.tum.de/ (at time of writing this is Isabelle2018). We provide a ROOT file in this repository with a number of heap images. Our Isabelle theories depend on a number of entries from the Archive of Formal Proofs (AFP), and without installing these dependencies you will not be able to start Isabelle/UTP. Our repository notably depends on the Optics session which provides support for lenses, which we use to model variables. Our hybrid systems modelling session UTP-Hybrid also depends on Ordinary Differential Equations.

The easiest way to build the key heap images is using the build scripts located in bin/utp-jedit.sh and bin/build.sh, which also handle fetching of appropriate AFP dependencies. utp-jedit.sh uses the jEdit interface to perform the build, and build.sh does a command line build, and also generates the documentation under doc/. Running either of these script will first attempt to download all the necessary libraries from the AFP, and will then build the main UTP heap images one by one.

Alternatively, you can follow the AFP instructions, which requires that you download and install the whole AFP first. Our build scripts rely on knowing the location of where Isabelle/UTP is installed. If they do not correctly guess the location then please set the environment variable ISABELLE_UTP to the absolute path where it is installed.

Either way, once the depedencies are installed and appropriate heap images built, you’re ready to go. If you wish to develop something using UTP, then you can use the heap image called UTP, that can be loaded by invoking

bin/utp-jedit UTP

from the command line in the installed directory. Alternatively you can configure your main Isabelle ROOTS file so that it knows about the location of Isabelle/UTP (see https://isabelle.in.tum.de/dist/Isabelle2018/doc/system.pdf). If you’re developing the Isabelle/UTP core you can instead invoke the UTP-Toolkit heap image. Various other heap images exist including:

Some of these heap images rely on other entries from the AFP. We therefore provide a utility under bin/ called afp_get.sh which fetches entries and places them in the contrib directory. For example, Ordinary Differential Equations can be obtained by running

bin/afp_get.sh Ordinary_Differential_Equations

from the main UTP root directory. Alternatively there is a script bin/build.sh which fetches all dependencies and builds all heap images, and thus may be an easier option for installation.


Isabelle/UTP is supported by projects INTO-CPS, RoboCalc, and CyPhyAssure