[doc] Primitive documentation for installation and usage.

Makefile

@@ -53,4 +53,4 @@ release:
 	dune-release opam pkg
 	dune-release opam submit
 
-.PHONY: release clean clean doc view-doc promote test docker uninstall install all
+.PHONY: release clean doc view-doc promote test docker uninstall install all

doc/contents.rst

+Table of content
+================
+
+.. toctree::
+   :maxdepth: 2
+   :caption: Contents:
+
+   installation
+   usage
+   modules

doc/index.rst

@@ -4,17 +4,33 @@
    contain the root `toctree` directive.
 
 Welcome to Caisar's documentation!
-==================================
+**********************************
+
+CAISAR (Characterizing AI Safety And Robustness) is a platform
+under active development at CEA LIST, aiming to provide a
+wide range of features to characterize the robustness of
+artificial intelligence based software.
+It is available as a free software under the LGPLV2.1
+license. Code is hosted at
+https://git.frama-c.com/pub/caisar.
+
+You may browse the documentation for :ref:`installation` and :ref:`usage`.
+
+
+Content
+=======
 
 .. toctree::
    :maxdepth: 2
    :caption: Contents:
 
+   installation
+   usage
+   modules
+
 
 
 Indices and tables
 ==================
 
-* :ref:`genindex`
-* :ref:`modindex`
 * :ref:`search`

doc/installation.rst

+.. _installation:
+
+Installation
+============
+
+For now, no binaries are provided. Installation must be made
+directly by compiling the source.
+It requires Ocaml package manager Opam, v2.1 or higher.
+
+
+For development, it is recommended you set-up your own
+Opam switch (an OCaml installation isolated from system
+libraries)::
+
+  git clone https://git.frama-c.com/pub/laiser/caisar.git && cd caisar
+  opam switch create --yes --no-install . ocaml-base-compiler.4.13.1  
+
+Install external dependencies:::
+
+  opam depext --yes ocplib-endian base fmt alt-ergo.2.4.0  
+  opam install . --deps-only --with-test --yes  
+
+Finally, run the compilation and the unit tests:::
+
+  make  
+  make test  
+

doc/modules.rst

+API documentation
+=================
+
+.. toctree::
+   :maxdepth: 4
+
+   nier_cfg

doc/usage.rst

+.. _usage:
+
+Usage
+=====
+
+Property verification
+---------------------
+
+CAISAR can be used to verify properties on neural networks.
+The prototype command is ``caisar verify --solver=SOLVER property.mlw``
+File property.mlw defines the goal you want to verify,
+written in the Whyml language.
+Example of .mlw files can be seen in tests folder.
+
+External verifiers detection
+----------------------------
+
+CAISAR relies on external verifiers to work. You must install
+them first, then point CAISAR to their location.
+To do so,
+use ``DIR=/path/to/solver/exec caisar config -d.``
+
+List of supported verifiers:
+
+* PyRAT
+* `Marabou <https://github.com/NeuralNetworkVerification/Marabou>`_
+* `SAVer <https://github.com/abstract-machine-learning/saver>`_
+
+List of actively developed supports:
+
+* Tools that support SMTLIB as inputs: `Alt-Ergo <https://alt-ergo.ocamlpro.com/>`_, `Z3 <https://github.com/Z3Prover/z3/wiki>`_, `Colibri <https://colibri.frama-c.com/>`_