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.

6.2. Setting up a development environment

6.2.1. With an Opam switch

Once an opam switch is setup, one needs to download ocaml language server, ocamlformat v0.25.1 and ocp-indent.

6.2.2. With nix-shell

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