docs/install.rst - 3p/nicta/cogent - Git at Google

 =========================
 Cogent Installation Guide
 =========================

 .. highlight:: bash


 In a Nutshell
 =============

 See :ref:`install-more-details` below for a more elaborate guide.

 0. We primarily support Debian-style Linux OS. Other \*nix systems should also work, provided
    your platform supports all the dependencies Cogent needs.
 1. Install `GHC <https://www.haskell.org/downloads/>`__. For supported versions of GHC,
    see the ``tested-with`` section of `cogent/cogent.cabal <https://github.com/NICTA/cogent/blob/master/cogent/cogent.cabal>`_.
 2. Install `Cabal <https://www.haskell.org/cabal/download.html>`__ *or*
    `Stack <https://docs.haskellstack.org/en/stable/README/>`__.

 .. note:: We say ``Cabal`` to mean the ``cabal-install`` tool, which is not the same as
    the ``Cabal`` library. In particular, the version of ``cabal-install`` is not
    necessarily the same as that of the ``Cabal`` library.

 3. Install `Alex <https://www.haskell.org/alex/>`__ and `Happy <https://www.haskell.org/happy/>`__.
 4. Clone the `Cogent repository <https://github.com/NICTA/cogent>`__.
    Suppose the Cogent repository is located ``$COGENT``. Upon this point you should be able to install
    the Cogent compiler and compile Cogent programs. Move to directory ``$COGENT/cogent``, and use
    either Cabal or Stack to build the Cogent compiler.

 .. note:: For ``cabal`` users, we require cabal version 3.0+ and we use the ``new-*`` commands.

 5. As a sanity check, you should be able to run ``make test-compiler`` in the ``$COGENT/cogent`` folder,
    and the tests should pass.
 6. To run verification, install `Isabelle-2019 <https://isabelle.in.tum.de/>`_ either from their
    website, or you can simply checkout the ``isabelle`` submodule in the Cogent repository.
    You also need to download `AutoCorres (v1.6) <http://ts.data61.csiro.au/projects/TS/autocorres/>`_.


 .. _install-more-details:

 Detailed Instructions
 =====================

 Dependencies
 ------------

 -  `The Glasgow Haskell Compiler (GHC) <https://www.haskell.org/>`__
 -  `Cabal <https://www.haskell.org/cabal/>`__  *or*
    `Stack <https://docs.haskellstack.org/en/stable/README/>`__
 -  `Alex <https://www.haskell.org/alex/>`__
 -  `Happy <https://www.haskell.org/happy/>`__
 -  `z3 <https://github.com/Z3Prover/z3>`__ (which is also included
    as a submodule for convenience)

 Install Cogent dependencies
 ---------------------------

 The GHC compiler and Cabal
 ^^^^^^^^^^^^^^^^^^^^^^^^^^

 Follow the instructions on the `Haskell Downloads page <https://www.haskell.org/downloads/>`__
 to install GHC. Any of the options (Minimal installer, Stack, or Haskell Platform) will work.

 .. note:: The supported versions of GHC and Cabal are specified
           in `cogent/cogent.cabal <https://github.com/NICTA/cogent/blob/master/cogent/cogent.cabal>`__.

 .. note:: On Linux you may also have to install ``libgmp-dev``. This can
           be done with the command

 ::

   sudo apt-get install libgmp-dev

 or the equivalent command for your Linux distribution.

 ``alex`` and ``happy``
 ^^^^^^^^^^^^^^^^^^^^^^

 ::

   cabal new-install alex happy

 or the equivalent commands using ``stack``.

 Usually, the executables are located ``$HOME/.cabal/bin/``. Make sure
 you add them to your ``$PATH``.

 ``z3`` SMT-solver
 ^^^^^^^^^^^^^^^^^

 .. note:: This is optional. You don’t have to install ``z3`` if you don’t
           plan to use Cogent’s type-level computation features (see :ref:`static-arrays`).

 Follow their `README.md <https://github.com/Z3Prover/z3/blob/b79440a21d404bcf0c2e34e83f1c04555342cfb9/README.md>`__.
 Make sure that the executable is included in your ``$PATH``. Alternatively you can use the included
 `submodule <https://github.com/Z3Prover/z3/tree/b79440a21d404bcf0c2e34e83f1c04555342cfb9>`__
 by ``git submodule update --init --recursive -- z3``.

 .. note:: We only tested against the snapshot checked-in in the
           `submodule <https://github.com/Z3Prover/z3/tree/b79440a21d404bcf0c2e34e83f1c04555342cfb9>`__.
           Similar versions of ``z3`` have a chance to work but is not guaranteed.

 Install Cogent
 --------------

 .. _optional-features:

 Optional features
 ^^^^^^^^^^^^^^^^^

 Cogent comes with several experimental (reads: very unstable) or
 additional features that you can opt-in. These features are (with the
 names of the respective flags in parentheses):

    1. built-in static arrays (``builtin-arrays``)
    2. documentation generation (``docgent``)
    3. property-based testing in Haskell (``haskell-backend``)

 Depending on which (combination of) features are needed, the
 dependencies will be different. By default, none of them are enabled. If
 you want them enabled, appropriate flags should be given while building
 Cogent (see below for instructions).

 There are three ways of building the Cogent compiler:

   * Stack (simple, more robust)
   * Makefile (simple, but can be fragile)
   * Cabal (also simple, and more advanced)

 Detailed instructions for each of them are given below:

 Build with Stack (simple, more robust)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 Stack_ is a cross-platform program for developing Haskell projects.
 To build Cogent with Stack, simply run ``stack build``.

 .. _Stack: https://docs.haskellstack.org/

 Build with Makefile (simple, but can be fragile)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 -  To configure, edit `config.mk <https://github.com/NICTA/cogent/blob/master/config.mk>`__. The default values
    should work for most people.
 -  Change the flags for building Cogent in that file.
 -  Run ``make`` or ``make dev``. The latter builds Cogent instead of
    installing it, which is more suitable for developers.

 For more info, run ``make help``.

 Build with Cabal (also simple, and more advanced)
 ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

 The ``Makefile`` calls Cabal under the hood. The new (3.0+) version of Cabal
 is made relatively easy to use. You can use ``cabal new-configure`` with relevant options
 to set the flags and compiler version that are desired. Or it can be set manually
 in a ``cabal.project.local`` file.
 After the configuration, Cogent can be easily installed by
 ``cabal new-install --installdir=<BINDIR>`` command, where ``<BINDIR>`` is the directory
 in which you want the ``Cogent`` executable to be placed. This location should be added
 to your ``$PATH``.


 Test your installation
 ----------------------

 1. Test files are in `cogent/tests <https://github.com/NICTA/cogent/tree/master/cogent/tests>`__.
    Run ``make`` with relevant targets.

 -  ``make tests`` runs the entire test suite, which is **not** what you
    would like to do in most cases, as it also tests some Isabelle/HOL proofs, which
    will take very long time.
 -  ``make test-compiler`` tests many of the compiler phases without involving Isabelle.
 -  There are individual tests that can be triggered by ``make test-*``.
    See ``make help`` for details.
 -  ``make examples`` builds a group of small but complete Cogent
    examples.

 2. Cogent compiler also comes with a small unit-test module. To run
    that, do this:

 ::

   $> cabal new-build
   $> cabal new-test


 .. _install-macos-hints:

 Testing on macOS
 ^^^^^^^^^^^^^^^^

 To run Cogent examples and some tests, you need a GNU compatible version
 of ``cpp`` installed in your ``PATH``. The default ``cpp`` installed on
 ``macOS`` isn't GNU compatible.

 A solution:

   1. Install Homebrew
   2. Run ``brew install gcc``. This will create symlinks ``gcc-8`` and ``cpp-8``
      (or whatever the latest gcc version number is) in ``/usr/local/bin`` to the newly installed version
      of ``gcc``.
   3. Provided ``ls /usr/local/bin/cpp`` outputs
      ``No such file or directory``, it should be safe to run
      ``ln -s /usr/local/bin/cpp-8 /usr/local/bin/cpp``.
   4. If ``which cpp`` doesn't print ``/usr/local/bin/cpp``, then running
      ``export PATH=/usr/local/bin:$PATH`` in any shell where you want run the
      examples will ensure that the correct version of ``cpp`` is used.

 Running ``make examples`` should now be successful.


 Common Issues and Troubleshooting
 =================================

 Cabal Version
 -------------

 Cogent currently relies on ``cabal >= 3.0``. Please ensure that you are using version 3.

 Missing Dependencies
 --------------------

 Before trying to build Cogent, ensure that ``happy`` and ``alex`` are installed with cabal/stack::

   cabal new-install happy
   cabal new-install alex
	=========================
	Cogent Installation Guide
	=========================

	.. highlight:: bash


	In a Nutshell
	=============

	See :ref:`install-more-details` below for a more elaborate guide.

	0. We primarily support Debian-style Linux OS. Other \*nix systems should also work, provided
	your platform supports all the dependencies Cogent needs.
	1. Install `GHC <https://www.haskell.org/downloads/>`__. For supported versions of GHC,
	see the ``tested-with`` section of `cogent/cogent.cabal <https://github.com/NICTA/cogent/blob/master/cogent/cogent.cabal>`_.
	2. Install `Cabal <https://www.haskell.org/cabal/download.html>`__ or
	`Stack <https://docs.haskellstack.org/en/stable/README/>`__.

	.. note:: We say ``Cabal`` to mean the ``cabal-install`` tool, which is not the same as
	the ``Cabal`` library. In particular, the version of ``cabal-install`` is not
	necessarily the same as that of the ``Cabal`` library.

	3. Install `Alex <https://www.haskell.org/alex/>`__ and `Happy <https://www.haskell.org/happy/>`__.
	4. Clone the `Cogent repository <https://github.com/NICTA/cogent>`__.
	Suppose the Cogent repository is located ``$COGENT``. Upon this point you should be able to install
	the Cogent compiler and compile Cogent programs. Move to directory ``$COGENT/cogent``, and use
	either Cabal or Stack to build the Cogent compiler.

	.. note:: For ``cabal`` users, we require cabal version 3.0+ and we use the ``new-*`` commands.

	5. As a sanity check, you should be able to run ``make test-compiler`` in the ``$COGENT/cogent`` folder,
	and the tests should pass.
	6. To run verification, install `Isabelle-2019 <https://isabelle.in.tum.de/>`_ either from their
	website, or you can simply checkout the ``isabelle`` submodule in the Cogent repository.
	You also need to download `AutoCorres (v1.6) <http://ts.data61.csiro.au/projects/TS/autocorres/>`_.


	.. _install-more-details:

	Detailed Instructions
	=====================

	Dependencies
	------------

	- `The Glasgow Haskell Compiler (GHC) <https://www.haskell.org/>`__
	- `Cabal <https://www.haskell.org/cabal/>`__ or
	`Stack <https://docs.haskellstack.org/en/stable/README/>`__
	- `Alex <https://www.haskell.org/alex/>`__
	- `Happy <https://www.haskell.org/happy/>`__
	- `z3 <https://github.com/Z3Prover/z3>`__ (which is also included
	as a submodule for convenience)

	Install Cogent dependencies
	---------------------------

	The GHC compiler and Cabal
	^^^^^^^^^^^^^^^^^^^^^^^^^^

	Follow the instructions on the `Haskell Downloads page <https://www.haskell.org/downloads/>`__
	to install GHC. Any of the options (Minimal installer, Stack, or Haskell Platform) will work.

	.. note:: The supported versions of GHC and Cabal are specified
	in `cogent/cogent.cabal <https://github.com/NICTA/cogent/blob/master/cogent/cogent.cabal>`__.

	.. note:: On Linux you may also have to install ``libgmp-dev``. This can
	be done with the command

	::

	sudo apt-get install libgmp-dev

	or the equivalent command for your Linux distribution.

	``alex`` and ``happy``
	^^^^^^^^^^^^^^^^^^^^^^

	::

	cabal new-install alex happy

	or the equivalent commands using ``stack``.

	Usually, the executables are located ``$HOME/.cabal/bin/``. Make sure
	you add them to your ``$PATH``.

	``z3`` SMT-solver
	^^^^^^^^^^^^^^^^^

	.. note:: This is optional. You don’t have to install ``z3`` if you don’t
	plan to use Cogent’s type-level computation features (see :ref:`static-arrays`).

	Follow their `README.md <https://github.com/Z3Prover/z3/blob/b79440a21d404bcf0c2e34e83f1c04555342cfb9/README.md>`__.
	Make sure that the executable is included in your ``$PATH``. Alternatively you can use the included
	`submodule <https://github.com/Z3Prover/z3/tree/b79440a21d404bcf0c2e34e83f1c04555342cfb9>`__
	by ``git submodule update --init --recursive -- z3``.

	.. note:: We only tested against the snapshot checked-in in the
	`submodule <https://github.com/Z3Prover/z3/tree/b79440a21d404bcf0c2e34e83f1c04555342cfb9>`__.
	Similar versions of ``z3`` have a chance to work but is not guaranteed.

	Install Cogent
	--------------

	.. _optional-features:

	Optional features
	^^^^^^^^^^^^^^^^^

	Cogent comes with several experimental (reads: very unstable) or
	additional features that you can opt-in. These features are (with the
	names of the respective flags in parentheses):

	1. built-in static arrays (``builtin-arrays``)
	2. documentation generation (``docgent``)
	3. property-based testing in Haskell (``haskell-backend``)

	Depending on which (combination of) features are needed, the
	dependencies will be different. By default, none of them are enabled. If
	you want them enabled, appropriate flags should be given while building
	Cogent (see below for instructions).

	There are three ways of building the Cogent compiler:

	* Stack (simple, more robust)
	* Makefile (simple, but can be fragile)
	* Cabal (also simple, and more advanced)

	Detailed instructions for each of them are given below:

	Build with Stack (simple, more robust)
	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

	Stack_ is a cross-platform program for developing Haskell projects.
	To build Cogent with Stack, simply run ``stack build``.

	.. _Stack: https://docs.haskellstack.org/

	Build with Makefile (simple, but can be fragile)
	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

	- To configure, edit `config.mk <https://github.com/NICTA/cogent/blob/master/config.mk>`__. The default values
	should work for most people.
	- Change the flags for building Cogent in that file.
	- Run ``make`` or ``make dev``. The latter builds Cogent instead of
	installing it, which is more suitable for developers.

	For more info, run ``make help``.

	Build with Cabal (also simple, and more advanced)
	^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

	The ``Makefile`` calls Cabal under the hood. The new (3.0+) version of Cabal
	is made relatively easy to use. You can use ``cabal new-configure`` with relevant options
	to set the flags and compiler version that are desired. Or it can be set manually
	in a ``cabal.project.local`` file.
	After the configuration, Cogent can be easily installed by
	``cabal new-install --installdir=<BINDIR>`` command, where ``<BINDIR>`` is the directory
	in which you want the ``Cogent`` executable to be placed. This location should be added
	to your ``$PATH``.


	Test your installation
	----------------------

	1. Test files are in `cogent/tests <https://github.com/NICTA/cogent/tree/master/cogent/tests>`__.
	Run ``make`` with relevant targets.

	- ``make tests`` runs the entire test suite, which is not what you
	would like to do in most cases, as it also tests some Isabelle/HOL proofs, which
	will take very long time.
	- ``make test-compiler`` tests many of the compiler phases without involving Isabelle.
	- There are individual tests that can be triggered by ``make test-*``.
	See ``make help`` for details.
	- ``make examples`` builds a group of small but complete Cogent
	examples.

	2. Cogent compiler also comes with a small unit-test module. To run
	that, do this:

	::

	$> cabal new-build
	$> cabal new-test



	.. _install-macos-hints:

	Testing on macOS
	^^^^^^^^^^^^^^^^

	To run Cogent examples and some tests, you need a GNU compatible version
	of ``cpp`` installed in your ``PATH``. The default ``cpp`` installed on
	``macOS`` isn't GNU compatible.

	A solution:

	1. Install Homebrew
	2. Run ``brew install gcc``. This will create symlinks ``gcc-8`` and ``cpp-8``
	(or whatever the latest gcc version number is) in ``/usr/local/bin`` to the newly installed version
	of ``gcc``.
	3. Provided ``ls /usr/local/bin/cpp`` outputs
	``No such file or directory``, it should be safe to run
	``ln -s /usr/local/bin/cpp-8 /usr/local/bin/cpp``.
	4. If ``which cpp`` doesn't print ``/usr/local/bin/cpp``, then running
	``export PATH=/usr/local/bin:$PATH`` in any shell where you want run the
	examples will ensure that the correct version of ``cpp`` is used.

	Running ``make examples`` should now be successful.


	Common Issues and Troubleshooting
	=================================

	Cabal Version
	-------------

	Cogent currently relies on ``cabal >= 3.0``. Please ensure that you are using version 3.

	Missing Dependencies
	--------------------

	Before trying to build Cogent, ensure that ``happy`` and ``alex`` are installed with cabal/stack::

	cabal new-install happy
	cabal new-install alex