Getting the Cogent Compiler

What follows is a very quick guide to setting up the Cogent compiler, enough to be able to write and compile code. To do anything more complex, including working on proofs, you should also read the full installation instructions.

Cogent’s compiler is still a work in progress: we don’t (yet) provide compiled executables, and it’s not (yet) available in package managers, so to install it, you’ll need to do some work.

We assume you’re running a recent *nix-like operating system: development primarily happens on recent versions of Debian GNU/Linux, and it’s highly likely that similar GNU/Linux systems will also work, possibly with some minor tweaks. macOS also generally works, although you may need to acquire some of the GNU development tools.

Install Haskell. An easy way to do this is using the Haskell Stack tool. If you’re not planning on actively developing Cogent, this is an excellent option.

Once you’ve installed Stack, get the Cogent source code using Git:

$ git clone https://github.com/NICTA/cogent.git
$ cd cogent/cogent
$ stack build

This will take several minutes, depending on how fast your system is, and how fast your Internet connection is. Once this finishes, you can use:

$ stack exec -- cogent

You can also copy the compiled executable to a more convenient location that might already be on your $PATH. To find out where the compiler is, run:

$ stack exec -- which cogent

For much of this document, we’ll assume that you can just run cogent to invoke the Cogent compiler.

For more information, check out the detailed installation instructions.