The easiest way to install Tamarin on macOS or Linux is to use Homebrew:
brew install tamarin-prover/tap/tamarin-prover
It’s separately packaged for
pacman -S tamarin-prover
nix-env -i tamarin-prover
You can install Tamarin (with GUI) under Windows 10 using the
Subsystem for Linux (WSL). For performance and compatibility
reasons, we recommend using WSL2 with Ubuntu. Once you have WSL
and Ubuntu installed, start the Ubuntu app and install Tamarin
following the installation instructions
for Linux above. You can then run Tamarin inside the the
Ubuntu app using the usual command. To use the interactive mode,
start Tamarin inside the app and connect your usual Windows-run
browser to http://127.0.0.1:3001. Your
Windows files are accessible inside the Ubuntu app via, e.g.,
/mnt/c for files on drive
You don’t need to compile Tamarin from source unless you are developing a new feature for it or you want to use an unreleased feature. However, if you do want to install it from source:
Tamarin requires Haskell Stack to build and GraphViz and Maude (2.7.1 or newer) to run. The easiest way to install these is
brew install tamarin-prover/tap/maude graphviz haskell-stack
Alternatively, you can install them yourself:
Haskell Stack Follow the instructions
given at Stack’s
install page. If you are installing
your package manager (particularly on Ubuntu), you must run
stack upgrade afterwards, as that version of
stack is usually out-of-date.
Graphviz Graphviz should be available using your standard package manager, or directly from http://www.graphviz.org/
Maude You can install Maude using your
package manager (make sure to have version 2.7.1. or newer). You
can also install Maude manually from the [Maude website]
In this case, you should ensure that your
includes the install path, so that calling
the right version. Note that even though the Maude executable is
prelude.maude file must be in the same
folder that you start Maude from.
Check out the source code with
git clone https://github.com/tamarin-prover/tamarin-prover.git
and you have the current development version ready for
compilation. If you would prefer to use the master version, just
git checkout master.
In either case, you can then run
make default in
the new directory, which will install an appropriate GHC (the
Glasgow Haskell Compiler) for your system, including all
tamarin-prover executable will be
~/.local/bin/tamarin-prover. Note that this
process will take between 30 and 60 minutes, as all dependencies
(roughly 120) are compiled from scratch. If you later pull a newer
version of Tamarin (or switch to/from the
branch), then only the tool itself needs to be recompiled, which
takes a few minutes, at most.
If you have access to a faster desktop or server, but prefer
using Tamarin on your laptop, you can do that. The cpu/memory
intensive reasoning part of the tool will then run on the faster
machine, while you just run the GUI locally, i.e., the web browser
of your choice. To do this, you forward your port 3001 to the port
3001 of your server with the following command, replacing
ssh -L 3001:localhost:3001 SERVERNAME
If you do this, we recommend that you run your Tamarin instance on the server in a screen environment, which will continue running even if the network drops your connection as you can later reconnect to it. Otherwise, any network failure may require you to restart Tamarin and start over on the proof.
Under the etc folder contained in the Tamarin Prover project, plug-ins are available for VIM, Sublime Text 3, Emacs and Notepad++. Below we details the steps required to install your preferred plug-in.
This example will use Vundle to install the plugin directly from this repository. The instructions below should be translatable to other plugin managers.
You can install updates through
If you install the Vim support files using this method, you will need to keep the files up-to-date yourself.
~/.vim/directory if not already existing, which is the typical location for
~/.vim/, including the folders.
editor-sublime is a plug-in developed for the Sublime Text 3 editor. The plug-in has the following functionality: - Basic Syntaxes - Snippets for Theories, Rules, Restrictions and Lemmas
editor-sublime can be install in two ways:
The first and preferred method is with PackageControl.io. editor-sublime can now be installed via the sublime package manager. See the install and usage documentation, then search and install TamarinProver.
Alternatively it can be installed from source. For Linux /
macOS this process can be followed. We assume you have the
git tool installed.
cd ~/Library/Application\ Support/Sublime\ Text\ 3/Packages/
git clone email@example.com:tamarin-prover/editor-sublime.git
git clone https://github.com/tamarin-prover/editor-sublime.git
Please be aware that this plugin is under active development and as such, several of the features are still implemented in a prototypical manner. If you experience any problems or have any questions on running any parts of the plug-in please visit the project GitHub page.
implements a SPTHY major mode. You can load it with
M-x load-file, or add it to your
in your favourite way.
package provides Tamarin syntax highlighting for Atom. To install
apm install language-tamarin.
To uninstall (and “untap” the Tamarin homebrew tap):
brew uninstall tamarin-prover
brew untap tamarin-prover/tap
Tamarin was previously distributed in the now-closed
homebrew-science tap. If you have already installed
it through Homebrew, you may have to uninstall and untap that
brew uninstall tamarin-prover
brew untap homebrew/science
stack upgrade and
stack update. An out-of-date stack version can cause
spurious compilation errors.