Setting up Agda on Debian

I wrestled with this for some days, but finally I figured it out.

Here’s a Bash script distilling the lessons I learned. The starting point is obviously Agda (quite cumbersome) documentation. I couldn’t manage to run anything installed from apt, therefore I went for the first method.

apt-get update

# libraries necessary to run Cabal later (I found these names by 'trial and error', YMMV)
apt-get install zlib1g-dev libncurses5-dev libgmp3-dev libnuma-dev -y

# install Haskell
apt-get install ghc ghc-prof ghc-doc -y
# install Cabal
apt-get install cabal-install -y
cabal update
cabal install Cabal cabal-install

# install Agda dependencies
cabal install alex happy Agda

# install the standard library ( from https://github.com/agda/agda-stdlib/blob/master/notes/installation-guide.md )

mkdir ~/.agda
cd ~/.agda
wget -O agda-stdlib.tar https://github.com/agda/agda-stdlib/archive/v1.0.1.tar.gz
tar -zxvf agda-stdlib.tar

cd agda-stdlib-1.0.1
cabal install
cd ..

echo "~./agda/agda-stdlib-1.0.1/standard-library.agda-lib" > libraries
# this allows references to the standard library in every Agda project
echo "standard-library" > defaults

# install Emacs
apt-get install emacs -y

# setup Agda tool for Emacs
agda-mode setup
agda-mode compile

I take this opportunity to say why I’m installing this.

I’m currently taking a course in type theory, and it ended with two guest lectures by prof. Philip Wadler, who taught us the basics of Agda. He followed his (and Kokke’s) new book Programming Language Foundations in Agda. It’s an “interactive” book, written in “literate Agda”, which is a way to write notebooks with Agda snippets inside.

The lectures were great and ended prof. Wadler performing a funny stunt:

He literally ripped off his shirt to show this t-shirt underneath.

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.