Getting Started with PLFA

Dependencies for users

You can read PLFA online without installing anything. However, if you wish to interact with the code or complete the exercises, you need several things:

PLFA is tested against specific versions of Agda and the standard library, which are shown in the badges above. Agda and the standard library change rapidly, and these changes often break PLFA, so using older or newer versions usually causes problems.

Installing Agda using Stack

The easiest way to install any specific version of Agda is using Stack. You can get the required version of Agda from GitHub, either by cloning the repository and switching to the correct branch, or by downloading the zip archive:

git clone https://github.com/agda/agda.git
cd agda
git checkout v2.6.0.1

To install Agda, run Stack from the Agda source directory:

stack install --stack-yaml stack-8.6.5.yaml

If you want Stack to use you system installation of GHC, you can pass the --system-ghc flag and select the appropriate stack-*.yaml file. For instance, if you have GHC 8.2.2 installed, run:

stack install --system-ghc --stack-yaml stack-8.2.2.yaml

Installing the Standard Library and PLFA

You can get the required version of the Agda standard library from GitHub, either by cloning the repository and switching to the correct branch, or by downloading the zip archive:

git clone https://github.com/agda/agda-stdlib.git
cd agda-stdlib
git checkout v1.1

You can get the latest version of Programming Language Foundations in Agda from GitHub, either by cloning the repository, or by downloading the zip archive:

git clone https://github.com/plfa/plfa.github.io

Finally, we need to let Agda know where to find the standard library. For this, you can follow the instructions here.

It is possible to set up PLFA as an Agda library as well. If you want to complete the exercises found in the courses folder, or to import modules from the book, you need to do this. To do so, add the path to plfa.agda-lib to ~/.agda/libraries and add plfa to ~/.agda/defaults, both on lines of their own.

Setting up and using Emacs

The recommended editor for Agda is Emacs with agda-mode. Agda ships with agda-mode, so if you’ve installed Agda, all you have to do to configure agda-mode is run:

agda-mode setup

To load and type-check the file, use C-c C-l.

Agda is edited “interactively, which means that one can type check code which is not yet complete: if a question mark (?) is used as a placeholder for an expression, and the buffer is then checked, Agda will replace the question mark with a “hole” which can be filled in later. One can also do various other things in the context of a hole: listing the context, inferring the type of an expression, and even evaluating an open term which mentions variables bound in the surrounding context.”

Agda is edited interactively, using “holes”, which are bits of the program that are not yet filled in. If you use a question mark as an expression, and load the buffer using C-c C-l, Agda replaces the question mark with a hole. There are several things you can to while the cursor is in a hole:

C-c C-c x    split on variable x
C-c C-space  fill in hole
C-c C-r      refine with constructor
C-c C-a      automatically fill in hole
C-c C-,      goal type and context
C-c C-.      goal type, context, and inferred type

See the emacs-mode docs for more details.

If you want to see messages beside rather than below your Agda code, you can do the following:

Open your Agda file, and load it using C-c C-l;
type C-x 1 to get only your Agda file showing;
type C-x 3 to split the window horizontally;
move your cursor to the right-hand half of your frame;
type C-x b and switch to the buffer called “Agda information”.

Now, error messages from Agda will appear next to your file, rather than squished beneath it.

Auto-loading `agda-mode` in Emacs

Since version 2.6.0, Agda has support for literate editing with Markdown, using the .lagda.md extension. One side-effect of this extension is that most editors default to Markdown editing mode, whereas In order to have agda-mode automatically loaded whenever you open a file ending with .agda or .lagda.md, put the following on your Emacs configuration file:

(setq auto-mode-alist
   (append
     '(("\\.agda\\'" . agda2-mode)
       ("\\.lagda.md\\'" . agda2-mode))
     auto-mode-alist))

The configuration file for Emacs is normally located in ~/.emacs or ~/.emacs.d/init.el, but Aquamacs users might need to move their startup settings to the Preferences.el file in ~/Library/Preferences/Aquamacs Emacs/Preferences.

Using mononoki in Emacs

It is recommended that you install the font mononoki, and add the following to the end of your emacs configuration file at ~/.emacs:

;; default to mononoki
(set-face-attribute 'default nil
                    :family "mononoki"
                    :height 120
                    :weight 'normal
                    :width  'normal)

Unicode characters

If you’re having trouble typing the Unicode characters into Emacs, the end of each chapter should provide a list of the unicode characters introduced in that chapter.

agda-mode and emacs have a number of useful commands. Two of them are especially useful when you solve exercises.

For a full list of supported characters, use agda-input-show-translations with:

M-x agda-input-show-translations

All the supported characters in agda-mode are shown.

If you want to know how you input a specific Unicode character in agda file, move the cursor onto the character and type the following command:

M-x quail-show-key

You’ll see the key sequence of the character in mini buffer.

Dependencies for developers

PLFA is available as both a website and an EPUB e-book, both of which can be built on Linux and macOS. PLFA is written in literate Agda with Kramdown Markdown.

Building the website

The website version of the book is built in three stages:

The .lagda.md files are compiled to Markdown using Agda’s highlighter. (This requires several POSIX tools, such as bash, sed, and grep.)
The Markdown files are converted to HTML using Jekyll, a widely-used static site builder. (This requires Ruby and Jekyll.)
The HTML is checked using html-proofer. (This requires Ruby and html-proofer.)

Most recent versions of Ruby should work. The easiest way to install Jekyll and html-proofer is using Bundler. You can install Bundler by running:

gem install bundler

You can install the remainder of the dependencies—Jekyll, html-proofer, etc.—by running:

bundle install

Once you have installed all of the dependencies, you can build a copy of the book, and host it locally, by running:

make build
make serve

The Makefile offers more than just these options:

make                      # see make test
make build                # builds lagda->markdown and the website
make build-incremental    # builds lagda->markdown and the website incrementally
make test                 # checks all links are valid
make test-offline         # checks all links are valid offline
make serve                # starts the server
make server-start         # starts the server in detached mode
make server-stop          # stops the server, uses pkill
make clean                # removes all ~unnecessary~ generated files
make clobber              # removes all generated files

If you simply wish to have a local copy of the book, e.g. for offline reading, but don’t care about editing and rebuilding the book, you can grab a copy of the master branch, which is automatically built using Travis. You will still need Jekyll and preferably Bundler to host the book (see above). To host the book this way, download a copy of the master branch, unzip, and from within the directory run

bundle install
bundle exec jekyll serve

Building the EPUB

The EPUB version of the book is built using Pandoc. Here’s how to build the EPUB:

Install a recent version of Pandoc, available here. We recommend their official installer (on the linked page), which is much faster than compiling Pandoc from source with Haskell Stack.
Build the EPUB by running:
```
make epub
```
The EPUB is written to out/epub/plfa.epub.