[doc] Clarify setting up the development environment

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

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