Compiling Agda 2.6.2 on Fedora 32

Agda is a dependently typed functional programming language that I like very much. Its latest versions have some special features which are not supported by any more well known languages, for example higher inductive types. Since I want to use all the special features of Agda, I regularly compile the latest version. This is a procedure which comes with a few surprises more often than not, so this post is about saving you the time it took me to figure out what to do.

I like to compile Agda using the Haskell tool Stack, which can be installed with

curl -sSL https://get.haskellstack.org/ | sh

The sources of Agda have to be checked out with all submodules – otherwise there will be some weird “cabal” (another Haskell tool, more basic than Stack) errors which I was not able to understand. This can be done with:

git clone --recurse-submodules https://github.com/agda/agda.git

Now if you go to the Agda folder

cd agda

There should be files called “stack-8.8.4.yaml” and similar. Those files can can tell Stack how to build Agda. The number is the version of the Haskell compiler which is used to build Agda. I usually use the latest, you do not have to figure out which (if any) is installed on your system, since Stack will just download the appropriate compiler for you.

However, just running stack failed for my on Fedora 32 due to some linking problem in the end. It turned out, that “libtinfo.so” was not found by the linker. “libtinfo.so.6” is available on Fedora 32, so adding a link to it fixed the problem:

sudo ln -s /usr/lib64/libtinfo.so.6 /usr/lib64/libtinfo.so

Now, you can tell Stack to get all necessary things and compile and install Agda with:

stack install --stack-yaml stack-8.8.4.yaml

This also installs a binary into “~/.local/bin” which is in PATH on Fedora 32 by default, so you should be able to call agda from the command line. Also, you can use “agda-mode” to configure emacs for agda.

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.