Skip to main content

Development Guide

This guide explains how Caesar and related tools work internally and how to contribute to the code.

The whole project currently lives in a GitHub repository: github.com/moves-rwth/caesar. We use GitHub's issue tracker.

Caesar

Caesar's's source code is begins at the root level of the Git repository. It is a cargo workspace containing the main caesar crate and the z3rro crate.

We try to use rustdoc as much as possible to document how caesar works. Just run cargo doc --open to build and open the Rust API documentation of the project.

To run all tests, execute cargo test --all.

The source code for the caesar crate lives in src/.

Integration tests live in the tests/ directory. Read the associated tests/README.md for more information about these tests.

z3rro is our dedicated crate for basic SMT functionality. It lives in z3rro/. The idea is that this code is independent of Caesar itself and may be useful to other projects.

pgcl2heyvl

pgcl2heyvl is our pGCL frontend. It lives in pgcl/pgcl2heyvl. The tool is written in Python and we use poetry for its dependency management. The most important dependency is probably which defines the accepted pGCL syntax.

The tool has a terrible user interface (need to specify invariants as command-line arguments!) and pgcl2heyvl is being phased out (see its documentation) in favor of integration of the encodings directly in Caesar.

Website

The documentation you are reading right now is built using Docosaurus and lives in the website directory.

You can install it using yarn or npm: Run yarn or npm install.

Then either run yarn start or npm run start to start a local development server and open the site in a browser window.