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.
  4. Install Alex and Happy.
  5. 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 provide a config file for each supported version of GHC, so that you always get consistent dependencies. These config files are located in cogent/misc/cabal.config.d. Move the one that matches your GHC version to $COGENT/cogent/cabal.config. Then run Cabal as normal.

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

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 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)

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:

  • Makefile (simple, but can be fragile)
  • Cabal (more advanced)
  • Stack (simple, more robust)

Detailed instructions for each of them are given below:

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

  • To configure, edit config.mk. The default values should work for most people.
  • Copy the config file of the GHC version you want to use from cogent/misc/cabal.config.d into the cogent folder, and then rename it to cabal.config.
  • 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.3. Build with Cabal (more advanced)

The Makefile calls Cabal under the hood. It installs Cogent using a Cabal sandbox. If this is not ideal for you (in rare cases), or you want to customise your installation further, just use Cabal in the normal way. You need to install isa-parser before you build/install Cogent.

Copy the config file of the GHC version you want to use from /cogent/misc/cabal.config.d into this folder, and then rename it to cabal.config, and change the flags at the very beginning of that config file accordingly. Alternatively, the flags can be overwritten if something like --flags="flag1 flag2" is given when running cabal configure and cabal install.

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

3.2.4. Test your installation

  1. Test files are in 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.
  1. Cogent compiler also comes with a small unit-test module. To run that, do this:
$> cabal configure --enable-tests
$> cabal build
$> cabal 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-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.

3.3. Common Issues and Troubleshooting

3.3.1. Cabal Version

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

3.3.2. Missing Dependencies

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

cabal install happy
cabal install alex

3.3.3. Could not resolve dependency isa-parser

You may see the following error message:

Resolving dependencies...
cabal: Could not resolve dependencies:
[__0] trying: cogent-2.9.0.0 (user goal)
[__1] unknown package: isa-parser (dependency of cogent)
[__1] fail (backjumping, conflict set: cogent, isa-parser)
After searching the rest of the dependency tree exhaustively, these were the
goals I've had most trouble fulfilling: cogent, isa-parser

isa-parser must be installed manually in this case. Change to the directory isa-parser at the root of the repository, and run cabal install. Then, retry installing/building Cogent.