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 inconfig/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