Agda

2-minute read
emacs • haskell

In preparation for the HoTTEST Summer School, I installed Agda.

Prerequisites

Debian provides all the Haskell packages required. I had already installed haskell-platform, which includes

And, of course, I had already installed Emacs! I also installed these other libraries

❯ sudo apt install zlib1g-dev libncurses5-dev
❯ sudo apt install libicu-dev

I tried installing agda from Debian (which includes agda-bin, agda-stdlib, and libghc-agda-dev), but it didn't work. I fussed with it for a bit, but eventually gave up and purged it. I installed from cabal instead

❯ cabal update
❯ cabal install Agda

Despite its name, Agda's standard library is installed separately

❯ cd ~/agda
❯ wget https://github.com/agda/agda-stdlib/archive/v1.7.1.tar.gz
❯ tar xf v1.7.1.tar.gz
❯ cd agda-stdlib-1.7.1
❯ cabal install

❯ cd 
❯ mkdir .agda
❯ cd .agda

❯ cat >> libraries
$HOME/agda/agda-stdlib-1.7.1/standard-library.agda-lib

❯ cat >> defaults
standard-library

I had trouble getting agda mode working in Emacs. Turns out it didn't like interactive mode, so I disabled it before loading the file.

(setq shell-command-switch "-c")

(load-file (let ((coding-system-for-read 'utf-8))
                (shell-command-to-string "agda-mode locate")))

(setq shell-command-switch "-ic")

Now we can write the "hello world" program in Agda!

./hello-agda.png

And compile and run it like so

❯ cd ~/agda
❯ agda --compile hello-world.agda
Calling: ghc -O -o /home/tim/agda/hello-world -Werror -i/home/tim/agda -main-is MAlonzo.Code.QhelloZ45Zworld /home/tim/agda/MAlonzo/Code/QhelloZ45Zworld.hs --make -fwarn-incomplete-patterns
Linking /home/tim/agda/hello-world ...

❯ ./hello-world 
Hello world!