INSTALL.md

Using the Dockerfile

If you want to try out HOL4P4 in a more containerised fashion, you can do so using Docker. First, install Docker which in Ubuntu can be done with

sudo apt-get install docker.io

Then, build and run the Docker image (in the root directory of this repo containing the Dockerfile):

docker build -t hol4p4 .
docker run -it hol4p4

Manual Installation for Ubuntu 22.04

This guide assumes a fresh install of Ubuntu 22.04.

Dependencies

• HOL4
• Petr4
• Git

Optional, for generating HOL4 definitions and documentation

• Python 3
• Ott

Installation

You may skip steps for components you already have installed.

First, navigate to the directory where you want to put the source code of Poly/ML and HOL4. Then, in the terminal:

1. Install a C compiler and Git

    sudo apt-get install build-essential git
   

2. Install Poly/ML 5.9.1

    git clone https://github.com/polyml/polyml.git
    cd polyml
    git checkout v5.9.1
    ./configure --prefix=/usr
    make
    sudo make install
    cd ..
   

3. Install HOL4 Trindemossen-1

    git clone https://github.com/HOL-Theorem-Prover/HOL.git
    cd HOL
    git checkout trindemossen-1
    poly < tools/smart-configure.sml
    bin/build
    cd ..
   

   If you are annoyed that bin/build gives errors when compiling SAT solvers, you may add the gcc flag -std=c++14 to their respective Makefiles. However, these errors should not affect this project.

   If you want to be able to persistently compile HOL4 theories from anywhere, edit ~/.bashrc, now adding:

    export PATH=$PATH:[installation directory]/HOL/bin
   

   where [installation directory] is substituted with the directory you cloned HOL4 in, then

    source ~/.bashrc
   

   Otherwise, if you don't want the HOL4 installation to be persistent on your system, simply run

    export PATH=$PATH:[installation directory]/HOL/bin
   

   in the terminal window you want to be able to compile HOL4 theories from.

4. Install OPAM

    sudo apt-get install opam
    opam init
   

   When prompted, make a choice whether to let OPAM set environment variables or not. Then run

    eval $(opam env --switch=default)
   

5. Clone HOL4P4 and install Petr4 0.1.3

   Navigate to the directory where you want to install this repo, and do the following:

    git clone https://github.com/kth-step/HOL4P4.git
    cd HOL4P4
   

   then clone Petr4 in this location (do this even if you intend to use an existing Petr4 installation, this allows HOL4P4 to access example .p4 files for validation):

    git clone https://github.com/verified-network-toolchain/petr4.git
    cd petr4
    git checkout 0.1.3
   

   Then, follow the instructions for installing Petr4 from source here, using version 0.1.12 of p4pp.

   Finally, do

    cd ..
    make hol
   

   This will build the HOL4 theories and associated libraries.

6. (Optional) Install Python 3 and the latest version of Ott

    sudo apt-get install python3
    opam repo add coq-extra-dev https://coq.inria.fr/opam/extra-dev
    opam pin add ott dev -k version
   

   This will allow you to re-export the HOL4 definitions in hol/p4Script.sml as well as the documentation in docs/semantics/p4_defs.tex from the Ott files in the ott directory.

You may need to repeat eval $(opam env) depending on your choice in step 4 in order to use ott in the terminal.

Building documentation

You can also use make docs/semantics/main.pdf to build the documentation of the semantics. This requires some latex dependencies:

sudo apt-get install texlive

How to edit and interact with theories

The same tools used to edit HOL4 theories and run the HOL4 REPL can also be used for this project. Specifically, we recommend Emacs - a full guide for using HOL4 with Emacs can be found here.

Automatic installation scripts for Ubuntu 22.04

The scripts directory contains installation scripts. These may be run when installing HOL4P4 e.g. on a fresh virtual machine by

scripts/install.sh