diff --git a/doc/contributing.rst b/doc/contributing.rst new file mode 100644 index 0000000000000000000000000000000000000000..9f46da7087df40b77e252464d42a89fffe872a67 --- /dev/null +++ b/doc/contributing.rst @@ -0,0 +1,47 @@ +.. _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 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 in our interpreted language. +* ``tests/`` are non-regression tests written in `dune cram test syntax <https://dune.readthedocs.io/en/stable/tests.html>`_. + + +Setting up a development environment +************************************ + +TODO + +.. 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 +* bug fixes