IVy Installation Instructions

These instructions will allow a basic installation of the IVy language and checker. This sequence worked well on a fresh install of Debian 11. Ubuntu 20.04 may come with additional installation steps, some of which are listed at the bottom of this document.

Because this involves strange configurations with Python and other common programs, it may be good to install in a Docker container or virtual machine.

NOTE: It is not the most up-to-date version, but the only version of IVy I've been able to get to work recently is a few versions old (it can be installed from the archived microsoft repository, rather than the new kenmcmil or formal-verification-research respository). You're welcome to try installing the new version, especially if you're confident you can document the resolution to the errors it produces.

Prerequisites

First and foremost, get your package repository up to date before trying to install anything from this file:

sudo apt-get update

IVy requires a great deal of prerequisites, but they can thankfully all be installed using the following sequence of commands:

sudo apt-get install python2 g++ cmake python-ply git python-tk tix pkg-config libssl-dev curl libreadline-dev

IVy relies on python pointing to python2.7 rather than python3, so execute the following to link then check the python command:

sudo ln /usr/bin/python2 /usr/bin/python
python --version

Correct output indicates the version is python2.7.

Installing Pip2 is a bit of a challenge on newer systems, but the following sequence has always worked for me:

curl https://bootstrap.pypa.io/pip/2.7/get-pip.py --output get-pip.py
sudo python get-pip.py
sudo ln /usr/local/bin/pip2 /usr/bin/pip2

Verify the version of pip, it should correspond to python2.7. Then create a link like we did with python2.

pip2 --version
sudo ln /usr/local/bin/pip /usr/bin/pip
pip --version

Now let's take care of the pygraphviz dependency, which is probably more involved than it should be:

sudo apt-get install graphviz graphviz-dev
sudo apt-get install build-essential autoconf libtool pkg-config python-opengl python-pil python-pyrex python-pyside.qtopengl idle-python2.7 qt4-dev-tools qt4-designer libqtgui4 libqtcore4 libqt4-xml libqt4-test libqt4-script libqt4-network libqt4-dbus python-qt4 python-qt4-gl libgle3 python-dev libssl-dev
sudo apt-get install python-dev graphviz libgraphviz-dev pkg-config
sudo apt-get install python-dev build-essential libssl-dev libffi-dev      libxml2-dev libxslt1-dev zlib1g-dev python-pip
sudo apt-get install libpcap-dev libpq-dev
sudo apt-get install build-essential libssl-dev libffi-dev python-dev
sudo pip install pygraphviz

Make sure you're in the folder you'd like to have IVy installed in. If you followed the dedicated VM or Docker advice, this is usually best left in the home directory (found by cd ~).

Cloning IVy

There are three main places you can get IVy from. The current repository is at github.com/kenmcmil/ivy but you'll need to take caution if you use it.

An old but more reliable repository is at github.com/microsoft/ivy and this is the one we recommend.

Clone the repository ensuring you have the submodule dependencies with the following:

git clone --recurse-submodules https://github.com/microsoft/ivy.git 

Then navigate into the IVy folder:

cd ivy

Building Submodules

Run the following to ensure your dependencies are installed:

sudo apt-get install cmake
sudo apt-get install libreadline-dev

Then you can actually build the submodules (DO NOT use sudo unless you want root to own all the dependency files).

python build_submodules.py

This will take a long time, and expect warnings but not errors. The last couple of lines should look something like this, but it might change if you choose to install a newer version:

DO NOT EXECUTE THESE COMMANDS; USE ONLY TO CHECK RESULTS:

[100%] Built target test-openssl.t
cp -a include/*.h include/picotls ../../ivy/include/
cp -a *.a ../../ivy/lib/

Now you're finally ready to install IVy.

Installing IVy

Next, install IVy using this command, still in the ivy directory:

sudo python setup.py install

This should take a minute or two, and the following line indicates correctness:

DO NOT EXECUTE THESE COMMANDS; USE ONLY TO CHECK RESULTS:

Finished processing dependencies for ms-ivy==1.7.0

The IVy graphical interface likely has other dependencies, including tkinter, but these should be straightforward to install should you need them.

Testing Installation

You should now have a working installation of IVy. Check it using the following:

cd examples/ivy
ivy_check client_server.ivy

Your output should not produce errors, and it should resemble the following:

DO NOT EXECUTE THESE COMMANDS; USE ONLY TO CHECK RESULTS:

    The following properties are assumed initially:
        client_server.ivy: line 6: (no name)

    The following action implementations are present:
        client_server.ivy: line 9: implementation of connect
        client_server.ivy: line 17: implementation of disconnect
        client_server.ivy: line 25: implementation of error

    The following program assertions are treated as assumptions:
        in action disconnect when called from the environment:
            client_server.ivy: line 20: assumption
        in action connect when called from the environment:
            client_server.ivy: line 12: assumption
        in action error when called from the environment:
            client_server.ivy: line 29: assumption

OK