Agda installation

Agda installation

(Copied from the Toledo page of the Formal Systems course.)

In order to work with Agda, it is essential that you have the Agda typechecker, the Agda mode for Emacs, and the Agda standard library installed. The easiest way to get this is to work on the computers in the lab (SOL N or SOL Z), where everything has already been installed for you (but do use the .emacs file, see below). Alternatively, you can install Agda and the Agda standard library v1.1 on your own machine:

In any case, the code you deliver should be accepted by Agda version using version 1.1 of the standard library (as installed in SOL N and SOL Z of the department), so you should make sure you’re working with that version. You can check your Agda version by opening a terminal and entering “agda -V”. Differences between versions of Agda and of the Agda standard library are not enormous, so it is feasible to work in a different version and use a computer at the department to make sure that everything type-checks with the aforementioned versions, after finishing your project. (Contact us in case this turns out to be not so easy.)

It is also recommended to use the emacs configuration file provided here. To do so, simply place the file .emacs in your home folder. (Note that you should call it “.emacs”, not “emacs”, but the uploading software didn’t like that idea.) You also have to do this if you are working on the computers in the lab! If you already have a .emacs file, you can edit it and add the contents of our .emacs file at the bottom.

Final note: the emacs extension rainbow-delimiters is very recommendable when programming in Agda, Haskell, Lisp or another delimiter-intensive language. (But it seems to have become incompatible with the Agda interaction mode for emacs.)