3. Cogent Installation Guide¶
3.1. In a Nutshell¶
See Detailed Instructions below for a more elaborate guide.
- We primarily support Debian-style Linux OS. Other *nix systems should also work, provided your platform supports all the dependencies Cogent needs.
- Install GHC. For supported versions of GHC,
see the
tested-with
section of cogent/cogent.cabal. - Install Cabal or Stack.
- Install Alex and Happy.
- 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.
- As a sanity check, you should be able to run
make test-compiler
in the$COGENT/cogent
folder, and the tests should pass. - 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):
- built-in static arrays (
builtin-arrays
)- documentation generation (
docgent
)- 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 tocabal.config
. - Change the flags for building Cogent in that file.
- Run
make
ormake 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.4. Test your installation¶
- 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-*
. Seemake help
for details. make examples
builds a group of small but complete Cogent examples.
- 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:
- Install Homebrew
- Run
brew install gcc
. This will create symlinksgcc-8
andcpp-8
(or whatever the latest gcc version number is) in/usr/local/bin
to the newly installed version ofgcc
.- Provided
ls /usr/local/bin/cpp
outputsNo such file or directory
, it should be safe to runln -s /usr/local/bin/cpp-8 /usr/local/bin/cpp
.- If
which cpp
doesn’t print/usr/local/bin/cpp
, then runningexport PATH=/usr/local/bin:$PATH
in any shell where you want run the examples will ensure that the correct version ofcpp
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.