3. Cogent Installation Guide

3.1. In a Nutshell

See Detailed Instructions below for a more elaborate guide.

  1. We primarily support Debian-style Linux OS. Other *nix systems should also work, provided your platform supports all the dependencies Cogent needs.
  2. Install GHC. For supported versions of GHC, see the tested-with section of cogent/cogent.cabal.
  3. Install Cabal or Stack.

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.

  1. Install Alex and Happy.
  2. Clone the Cogent repository. 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.

  1. As a sanity check, you should be able to run make test-compiler in the $COGENT/cogent folder, and the tests should pass.
  2. To run verification, install Isabelle-2019 either from their website, or you can simply checkout the isabelle submodule in the Cogent repository. You also need to download AutoCorres (v1.6.1).

3.2. Detailed Instructions

3.2.1. Dependencies

3.2.2. Install Cogent dependencies

3.2.2.1. The GHC compiler and Cabal

Follow the instructions on the Haskell Downloads page 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.

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.

3.2.2.2. 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.

3.2.2.3. 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 Static arrays).

Follow their README.md. Make sure that the executable is included in your $PATH. Alternatively you can use the included submodule by git submodule update --init --recursive -- z3.

Note

We only tested against the snapshot checked-in in the submodule. Similar versions of z3 have a chance to work but is not guaranteed.

3.2.3. Install Cogent

3.2.3.1. 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)
  4. LLVM backend (llvm-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:

3.2.3.2. 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 in the cogent directory in which stack.yaml is located. We provide such config files (stack-<ghc-version>.yaml) for several different stack snapshots.

3.2.3.3. Build with Makefile (simple, but can be fragile)

  • To configure, edit 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.

3.2.3.4. 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.

3.2.4. Test your installation

  1. Run make with relevant targets in the cogent directory.
  • 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. The test files are grouped in sub-directories under cogent/tests/tests.
  • make examples builds a group of small but complete Cogent examples. The examples are located in cogent/examples. You can run make in each example’s directory to build them individually.
  1. Cogent compiler also comes with a small unit-test module. To run that, do this:
$> cabal new-build
$> cabal new-test

3.2.4.1. 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-11 and cpp-11 (or whatever the latest gcc version number is) in /usr/local/bin to the newly installed version of gcc.
  3. Set environment variables CC and CPP to your newly install
    GNU CC gcc-11 and GNU CPP cpp-11 (adapt to your version number) in the shell in which you want to run the tests.

Running make examples should now be successful.

3.3. Common Issues and Troubleshooting

3.3.1. Cabal Version

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

3.3.2. 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