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!
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!