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