.. _contributing:

Hacking CAISAR
==============
.. index:: single: Driver; driver

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 <https://dune.readthedocs.io/en/stable/tests.html>`_.
* ``utils/`` are helper functions used internally by CAISAR (for instance, logging utilities).
* ``vendor/`` contains scripts to build external provers for CAISAR


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.

.. _devdeps:

Additional dependencies
-----------------------
* `ocamlformat <https://github.com/ocaml-ppx/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 <https://github.com/ocaml/ocaml-lsp>`_ is optional
  but will vastly improve your development experience with OCaml.

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

With Nix
________________

Once Nix is setup as detailed in :ref:`nix`, typing `nix develop` will create a
shell environment tailored for CAISAR development. You can build CAISAR by
following the :ref:`source` instructions.

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.


.. index:: Prover;prover

Opening a merge request
***********************

We gladly accept merge requests (MR) on our `public forge <https://git.frama-c.com/pub/caisar/-/merge_requests>`_.
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