Skip to main content

Development Guide

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

The project is maintained in a GitHub repository: github.com/moves-rwth/caesar. We use GitHub's issue tracker. Feel free to open an issue or start a discussion. You can also reach the main developer, Philipp Schröer, by email: phisch@cs.rwth-aachen.de. We are very happy to work and research with you on Caesar!

Caesar​

Follow the "Build From Source" section in the installation instructions to learn how to compile Caesar. This gives you an environment to modify the code and run it locally.

The source code of the main caesar tool 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.

Website​

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

Use Node.js 24, as in CI, and Yarn Classic 1.22. Run yarn install --frozen-lockfile in website to install the dependencies from the committed lockfile.

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

VSCode Extension​

Caesar's VSCode extension lives in the vscode-ext/ directory. See vscode-ext/DEVELOPMENT.md for setup, debugging, tests, and packaging.

pgcl2heyvl​

pgcl2heyvl is our old 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.