These instructions apply to any UNIX-like system, including GNU/Linux, most BSD variants, Solaris, Cygwin on Windows, MacOSX, etc.
Notes for Windows users:
gcc4
, make
,
wget
, perl
. Install them using
Cygwin's setup.exe
.TLAPS tarball: tlaps-1.4.5.tar.gz
You can unpack TLAPS by running the following command:
This creates a directory named tlaps-1.4.5
that
contains four subdirectories: tlapm
, zenon
,
isabelle
and emacs
.
TLAPS is implemented in OCaml and requires version 4.04.2 or
higher. You can follow any of the suggestions
on the offical
OCaml release page to install OCaml. On Windows/Cygwin, OCaml
can be installed directly from Cygwin's setup.exe
.
On most modern
GNU/Linux distributions, OCaml is already packaged. Here are the
commands for the common Linux distributions:
Debian, Ubuntu, etc. | apt-get install ocaml |
Redhat, Fedora, SuSe, Mandriva, CentOS, etc. |
yum install ocaml |
Gentoo | emerge ocaml |
Arch Linux | pacman install ocaml |
On MacOSX, you can use the package
managers Homebrew
(brew install objective-caml
)
or MacPorts
(port install ocaml
).
If you want to install OCaml from source, consider using OPAM.
Run the following commands.
By default, the above will try to install
in /usr/local
. If you don't have write access to that
directory, or would rather install Zenon elsewhere, such as
in $HOME/bin
, run the following:
Follow the instructions on the Isabelle Web site. TLAPS actually does not need the full Isabelle2011-1 distribution. If you want only the necessary components, run the following commands:
You may
replace /usr/local
above by any other directory. For
example, to install Isabelle2011-1 in your $HOME
,
use -C $HOME
instead of -C /usr/local
.
Note that the isabelle
and isabelle-process
executables (found
in /usr/local/Isabelle/bin
or $HOME/Isabelle/bin
), or symbolic links to them, must
be in your $PATH
for TLAPS to work.
You may delete the Isabelle2011-1.tar.gz
and
polyml-5.4.0.tar.gz
files after the above steps.
Run the following commands.
(Replace /usr/local
above with wherever you
installed Isabelle in the previous step.)
Run the following commands.
By default, the above will try to install TLAPM
in /usr/local
. If you don't have write access to that
directory, or would rather install the TLAPM
elsewhere,
such as in $HOME/bin
, run the following:
Run the following command:
It should report the versions of zenon
and isabelle
you installed in earlier steps.
You can also test the TLAPS
on any of the examples
in the /usr/local/lib/tlaps/examples
directory (which
you can easily refer to using the option -I +examples
to tlapm
). For instance:
You will see a lot of output from Isabelle, the most important being the message at the end stating that all obligations were proved. For more information on how to use TLAPS, read the tutorial.