diff --git a/doc/contributing.rst b/doc/contributing.rst index 76d8393590ac30299ba1b013d261cdf8a38cb211..5c99edea64451da48c08046884184155aae5ced7 100644 --- a/doc/contributing.rst +++ b/doc/contributing.rst @@ -33,18 +33,64 @@ The root of the repository has the following folders: 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 +* `ocp-indent <https://github.com/OCamlPro/ocp-indent>`_ helps properly + indenting OCaml code +* 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, one needs to download `ocaml language server <https://github.com/ocaml/ocaml-lsp>`_, `ocamlformat <https://github.com/ocaml-ppx/ocamlformat>`_ v0.25.1 and `ocp-indent <https://github.com/OCamlPro/ocp-indent>`_. +Once an opam switch is setup, +type `opam install ocaml-lsp ocp-indent=VERSION ocamlformat` where +`VERSION` is specified in `.ocamlformat`. -With nix-shell --------------- +To setup the python test environment, +`python3 -m pip install -r tests/requirements.txt`. + +With nix develop +________________ With nix 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 @@ -57,3 +103,4 @@ Some possible topics for opening a MR are: * enhancing the support for an existing prover * new proof strategies * bug fixes +* enhancing of the documentation diff --git a/doc/installation.rst b/doc/installation.rst index 5251e2b0c9733e57566cf3273ad39ca2be2be62c..e1705c426718fabc77a4a719ed27d735b8a5f579 100644 --- a/doc/installation.rst +++ b/doc/installation.rst @@ -126,3 +126,9 @@ To run the tests: .. code-block:: console $ make test + +To build the documentation: + +.. code-block:: console + + $ make doc