6. Hacking CAISAR

6.1. CAISAR project structure

The root of the repository has the following folders:

  • bin/ contains utils for instanciating python-based prover for CAISAR.

  • ci/caisar-public/ contains automated scripts for replicating CAISAR repository on partner forges.

  • config/ contains various utilities for CAISAR to interface with external provers. In particular, driver definitions are located in config/drivers/.

  • doc/ contains all material related to documentation generation.

  • docker/ contains utils to build the CAISAR docker image for release.

  • examples/ contains examples of WhyML files representing known properties that CAISAR can verify.

  • lib/ contains OCaml library files that are primarly written to interface with CAISAR, but can be used in other projects as well.

  • licenses/ contains license files.

  • src/ contains most of the OCaml source of CAISAR.

  • stdlib/ contains WhyML files used to define theories for the CAISAR interpreted language.

  • tests/ are non-regression tests written in dune cram test syntax.

  • utils/ are helper functions used internally by CAISAR (for instance, logging utilities).

6.2. Setting up a development environment

The first step of contributing to CAISAR is to setup a development environment. Conforming with those instructions ensures all contributors share a common configuration. Common code formatting reduce the size of committed changes, focusing our attention on meaningful modifications only. Setting up the testing infrastructure allow to not introduce regressions in the codebase.

6.2.1. Additional dependencies

  • ocamlformat is a formatter for OCaml code. It must be installed with the version specified in the .ocamlformat file at the root of the directory;

  • a python3 interpreter version 3.9 of higher is required for tests and building documentation. Packages onnx and sphinx which version are specified under the tests/requirements.txt file are required;

  • a modern LaTeX compiler such as lualatex to compile the documentation;

  • the ocaml language server is optional but will vastly improve your development experience with OCaml.

6.2.1.1. With an Opam switch

Once an opam switch is setup, type opam install ocaml-lsp ocp-indent=VERSION ocamlformat where VERSION is specified in .ocamlformat.

To setup the python test environment, python3 -m pip install -r tests/requirements.txt.

6.2.1.2. With nix develop

With nix setup as detailed in Install through Nix, typing nix develop will create a shell environment tailored for CAISAR development. You can build CAISAR by following the Compile from source instructions.

6.2.2. Good development practices

Ensure that the code you commit is properly formatted and indented, compiles and passes local tests. It is possible to commit changes that temporary violate tests, as long as tests are passing for the final contributions.

All meaningful change in CAISAR should be propertly documented:

  • with clear and concise commit messages

  • with documentation of the interface and of the implementation for critical parts, to ease reviews and future modifications

  • with additions to the present manual

Developments are made on a separate branch that is up to date with master. Once the review is done, the branch is rebased against the latest master revision and then merged.

6.3. Opening a merge request

We gladly accept merge requests (MR) on our public forge. Some possible topics for opening a MR are:

  • support for a new prover

  • enhancing the support for an existing prover

  • new proof strategies

  • bug fixes

  • enhancing of the documentation