Installation#

Linux / macOS#

Sandboxing

We use esy for dependency management, which sandboxes dependencies. Apart from a few external dependencies (i.e. esy itself), installing Gillian will not affect your environment (including your opam switches)

It should be perfectly safe (and recommended) to install the development environment directly on your machine.

  1. Install prerequisites

    On Debian or Ubuntu, run:

    sudo apt install git curl npm build-essential pkg-config \
    m4 python3-distutils python3-apt

    On macOS, make sure you have the XCode command line tools installed:

    xcode-select --install

    …then make sure your development tools are up to date.

  2. Install esy

    npm install -g esy

  3. Clone the source repository

    Note

    If you are evaluating Gillian as an artifact, please use the source code provided to you as part of the artifact submission.

    git clone https://github.com/GillianPlatform/Gillian.git

  4. Prepare dependencies and build Gillian

    cd Gillian
esy install
esy build

    This may take a while, as esy will install and build sandboxed versions of every dependency, including OCaml and Z3.

    The #1 programmer excuse for legitimately slacking off: "I'm building Z3"

Windows#

Gillian is not supported on (native) Windows, but works fine through WSL (more specifically, default Ubuntu on WSL2).

Docker#

You can build a docker image from the source code:

git clone https://github.com/GillianPlatform/Gillian.git
cd Gillian
docker build -t gillian .

Once built, run Gillian with

docker run -it gillian

This will start the container and give you access through a zsh shell.

Inside the container, you’ll find:

  • The Gillian repository in /app/Gillian

  • Our fork of Test262 in /app/test262

  • Our fork of Collections-C in /app/collections-c

Testing your setup#

After installing and building (or entering the docker container), try running the following tests.

Gillian-JS#

esy x gillian-js verify Gillian-JS/Examples/JaVerT/BST.js --silent

Expected output

Obtaining specs to verify.
Obtained 5 symbolic tests
Running symbolic tests: 0.080211
Verifying one spec of procedure makeNode... Success
Verifying one spec of procedure find... Success
Verifying one spec of procedure findMin... Success
Verifying one spec of procedure remove... Success
Verifying one spec of procedure insert... Success
All specs succeeded: [Time]

Gillian-C#

esy x gillian-c bulk-exec Gillian-C/examples/concrete

Expected output

Registering tests...
Running 1 test suite
PASS  .

Test Suites: 0 failed, 1 passed, 1 total
Tests:       0 failed, 6 passed, 6 total
Time:        [Time]