Installation Overview
- Install Isabelle 2018
- Add the
Isabelle2018/bin
directory to yourPATH
variable - 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:
- Compilation may take a little time, so make some tea or coffee
- When the window disappears, go to
File > Open...
, and try to loadtutorial/utp_hello_world.thy
and see if it works
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 script located in bin/build.sh
, which also handles
fetching of appropriate AFP dependencies. Running this 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:
UTP-Designs
- theory of designs: imperative programs with total correctnessUTP-Reactive
- theory of Generalised Reactive ProcessesUTP-Reactive-Designs
- Reactive DesignsUTP-Circus
- Circus modelling languageUTP-Hybrid
- hybrid relational calculus
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