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​

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 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.

VSCode Extension​

Caesar's VSCode extension lives in the vscode-ext/ directory. The vscode-ext/vsc-extension-quickstart.md document explains the basics of how to develop and debug the binary.

Here, we still use npm for package management.

  • npm install to install the necessary dependencies.
  • npm run compile to compile the extension and run the linter.
  • npm run watch to start a TypeScript compiler server that recompiles when changes are made.
  • npm run lint to run the linter.
  • npm run vscode:prepublish compiles as well.

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.