.. _installation:

Installation
============

The latest release of CAISAR is available as an
`opam <https://opam.ocaml.org/>`_ package or
a `Docker <https://www.docker.com/>`_ image on GNU/Linux.
CAISAR is available on Windows either under the `Windows
Subsystem Linux <https://learn.microsoft.com/en-us/windows/wsl/install>`_ (WSL) or the aforementioned docker image.

The development version of CAISAR is available only by compiling the source code.
CAISAR needs access to a ``python3`` interpreter, which is
a default in all major GNU/Linux distributions.

Install through Opam
--------------------

This method requires requires the OCaml package manager
(Opam) v2.1 or higher to be installed in your system.
It is typically avaible in all major GNU/Linux distributions.

To install CAISAR via opam, do the following:

.. code-block:: console

   $ opam install caisar

Install through Docker
----------------------

This method requires Docker to be installed in your system.
A ready-to-use Docker image of CAISAR is available on
`Docker Hub <https://hub.docker.com>`_. To retrieve it, do the
following:

.. code-block:: console

   $ docker pull laiser/caisar:pub

Alternatively, a Docker image for CAISAR can be
created locally by proceeding as follows:

.. code-block:: console

   $ git clone https://git.frama-c.com/pub/caisar
   $ cd caisar
   $ make docker

To run the CAISAR Docker image, do the following:

.. code-block:: console

   $ docker run -it laiser/caisar:pub sh

.. _nix:

Install through Nix
-------------------

This method requires Nix (version 2.15 or above) to be installed on your system.

From Nixpkgs
************

CAISAR is currently not directly available on Nixpkgs. This should change for
the future release.

Using Nix flake
***************

A CAISAR `flake <https://nixos.wiki/wiki/Flakes>`_ is available at the root of
CAISAR directory. At the time of writing, flakes are still considered
experimental by NixOS. Hence, to use it, you will need to enable them following
the official Nix `instructions <https://nixos.wiki/wiki/Flakes#Temporary>`_.

Assuming you have Nix installed and are at the CAISAR repository root, you can
build CAISAR using the following command:

.. code-block:: console

   $ nix build

.. warning ::
   This command will fetch the Nixpkg registry for all build dependencies.
   This will result in several megabytes download. Make sure you have
   a stable network connexion before attempting building through Nix.

The CAISAR binary will reside in ``result/bin/caisar``. The manual will be under ``result/share/doc/ocaml4.14.1-caisar-${VERSION}/``.

You can run the CAISAR test suite using the following command:

.. code-block:: console

   $ nix flake check

You can setup a development environment with all CAISAR dependencies included using
`nix develop
<https://nixos.org/manual/nix/stable/command-ref/new-cli/nix3-develop.html>`_.
It will contain the ocaml toolchain already setup and installed, and the ocaml language server and formatter. You can thus compile and test CAISAR in an isolated shell.

.. code-block :: console

   $ nix develop

Finally, for experimental purposes, an environment comprised of CAISAR and several provers
is provided. 

.. code-block :: console

   $ nix build .#caisar_solver


.. note ::
   It is possible to use all those commands without cloning the git repository,
   for instance to quickly try CAISAR without installing it.
   To do so, specify the CAISAR flake location following
   `the official documentation
   <https://nix.dev/manual/nix/2.24/command-ref/new-cli/nix3-flake.html#flake-references>`_. 
   For instance, to create a shell where CAISAR is installed, use the following command:

   ``nix shell git+https://git.frama-c.com/pub/caisar.git --no-write-lock-file``




.. _source:

Compile from source
-------------------

To build and install CAISAR, do the following (this may take
some time, as it will download a full OCaml toolchain,
required dependencies and compile them):

.. code-block:: console

   $ git clone https://git.frama-c.com/pub/caisar
   $ cd caisar
   $ opam switch create --yes --no-install . 4.13.1
   $ opam install . --deps-only --with-test --yes
   $ make
   $ make install

To run the tests:

.. code-block:: console

   $ make test

To build the documentation:

.. code-block:: console

   $ make doc