Installation

This section shows how to build the nano-p4spectec binary from the P4-SpecTec source. You will use it along with make throughout the tutorial.

Cloning the Repository

$ git clone https://github.com/kaist-plrg/p4-spectec.git
$ cd p4-spectec
$ git checkout gsoc-nano-spec

Note: All exercises and the nano-p4spectec binary used throughout this tutorial are on the gsoc-nano-spec branch. Make sure you are on that branch before building.

Building from Source

Prerequisites

Linux

$ apt-get install opam
$ opam init

macOS

Install opam version 2.0.5 or higher following the instructions at ocaml.org.

You may also need libgmp-dev and pkg-config depending on your system.

NixOS

If you use Nix, a flake.nix is provided that sets up the full development environment automatically:

$ nix develop
$ make release

This drops you into a shell with OCaml 5.1 and all required packages available, without needing to manage opam manually.

OCaml Compiler and Packages

$ opam switch create 5.1.0
$ eval $(opam env)
$ opam install dune bignum 'menhir=20240715' 'menhirLib=20240715' core core_unix bisect_ppx yojson ppx_deriving_yojson

Building

$ make release

This creates the nano-p4spectec executable in the project root.