IVy Installation Notes

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

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

sudo apt-get update
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.7.

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 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 python-dev graphviz libgraphviz-dev pkg-config python-dev build-essential libssl-dev libffi-dev      libxml2-dev libxslt1-dev zlib1g-dev python-pip libpcap-dev libpq-dev build-essential libssl-dev libffi-dev python-dev cmake libreadline-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.

Getting IVy and Submodules

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 
cd ivy
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:

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

Building and Installing IVy

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

sudo python setup.py install

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:

   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