Some tips on working with Agda

Perhaps the greatest barrier to working with Agda might be setting up the required tools on your own machine. I have only done this on Mac OS X, and I did run into some issues (which, fortunately, I could solve). If you are using Windows or Linux, I don’t have much advice for you.

Agda interaction is best managed with the Emacs text editor. Other alternatives are less supported and more buggy. This means you need to install the current versions of Haskell, Emacs, Agda, and the Agda standard library (a separate install step).

On OS X, you can try to do everything through Homebrew, or you can try installing the various components separately. You can’t mix and match, because there seems to be no way to tell Homebrew that you’ve already installed part of what it needs. I installed Emacs through Homebrew, Haskell using the Haskell Platform, and Agda from source. It takes a long time to build it from source.

Emacs: https://www.gnu.org/software/emacs/
Haskell: https://www.haskell.org
Agda: https://agda.readthedocs.io/

You will need to configure Emacs to automatically use Agda mode when a file with the .agda (or .lagda for "literate" files) extension is loaded. This is typically done as part of Agda installation but sometimes it doesn’t work properly and you have to edit your .emacs initialization file.

You don’t need to know a lot of Emacs to work with Agda, but you need to know the basics. You can use the mouse (unless you’re remotely logged into a server, in which case some important keyboard shortcuts may not work properly). Arrow keys should work. But learning some basic keyboard commands will speed things up for you. There is a built-in tutorial, which you can run by typing C-h t. (That’s control and h together, followed by t.) Take notes, especially on how to exit Emacs. A lot of what’s in the tutorial isn’t necessary (all the C-u stuff) but you should learn basic navigation, cut-and-paste, and search. Here are some commands mentioned in the tutorial, separated here by semicolons, that I find useful and recommend to you.

C-x C-c; C-x k; C-g; C-v; M-v; C-l; C-p; C-n; C-b; C-f; M-f; M-b C-a; C-e; M-<; M->; C-x 1; C-<SPC>; C-w; C-y; M-y; C-/; C-x C-f; C-x C-s; C-x C-b; C-x b; C-s; C-r

The Agda documentation can be frustrating. I don’t understand its organization, and parts are incomplete. There are too few people involved, and they have a lot of things to do. I shouldn’t complain, as I haven’t attempted to contribute. I’m just warning you.

The documentation for Agda Emacs mode is fairly brief. I still don’t know what many of the commands do. Fortunately, we can get along with relatively few commands.

You shouldn’t be browsing in the Agda standard library until you are done with LACI, but if you want to use it for your own work, you will need to become familiar with its structure. The entire source is on GitHub, but there is also a site hosting an HTML version that has nice cross-links and some useful README files.

Agda standard library browser: https://agda.github.io/agda-stdlib/index.html