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: