The Petr4 project is developing the formal semantics of the P4 Language backed by an independent reference implementation.

See https://verified-network-toolchain.github.io/petr4/ or check out the gh-pages branch for information on the Petr4 artifact.

1. Install OPAM 2 following the official OPAM installation instructions. Make sure opam --version reports version 2 or later.

2. (on Linux) Install external dependencies:

   sudo apt-get install m4 libgmp-dev
   

3. (on MacOS) Install external dependencies:

   brew install m4
   brew install gmp
   

You can use the scripts to install Petr4. Alternatively, follow theses steps:

1. Check the installed version of OCaml:

   ocamlc -v
   

   If the version is less than 4.14.0, upgrade:

   opam switch create <name> ocaml-base-compiler.4.14.0
   

2. Install p4pp from source.

   opam pin add p4pp https://github.com/cornell-netlab/p4pp.git
   

3. Install Coq and Bignum.

   opam install coq
   opam install bignum
   

   If this doesn't work, install the dependencies manually. This step shouldn't be needed.

   opam install ANSITerminal alcotest bignum cstruct-sexp pp ppx_deriving ppx_deriving_yojson yojson js_of_ocaml js_of_ocaml-lwt js_of_ocaml-ppx
   

4. Build bundled dependencies.

   opam repo add coq-released https://coq.inria.fr/opam/released
   opam pin add coq-vst-zlist https://github.com/PrincetonUniversity/VST.git
   opam install . --deps-only
   

5. Use dune to build and install petr4.

   dune build
   dune install
   

6. [Optional] Run tests

   make test
   

7. [Optional] Install helper packages

   opam install utop ocaml-lsp-server ocamlformat ocamlformat-rpc
   

8. [Optional] Run one of the following commands dune utop OR dune utop -p petr4. Check if you can run the following command in the toplevel. It should return an empty string.

   Petr4.P4info.to_string Petr4.P4info.dummy;;   
   

Currently petr4 is merely a P4 front-end. By default, it will parse a source program to an abstract syntax tree and print it out, either as P4 or encoded into JSON.

Run petr4 -help to see the list of currently-supported options.

Petr4 is an open-source project. We encourage contributions! Please file issues on Github.

See the list of contributors.

Petr4 is released under the Apache2 License.