Writing Agda blog posts in literate markdown

Posted by Jesper on July 9, 2019

So you got to admit all the cool kids are doing it nowadays: writing blog posts in literate Agda. Do you want to join the club? Then you’ve come to the right place! In this blog post I’ll explain how to write a blog post (or any literate Agda code, really) as a markdown file and transform it into fancy highlighted and hyperlinked html. Don’t worry, it’s easy!

open import Agda.Builtin.Nat
open import Agda.Builtin.Equality

plus1 : (x : Nat) → x + 1 ≡ suc x
plus1 zero                    = refl
plus1 (suc x) rewrite plus1 x = refl

Writing the blog post

To start, you’ll first need to install Agda 2.6.0 or newer and Pandoc 2.2 or newer. Both can be installed from Cabal with cabal install agda-2.6.0.1 pandoc-2.2.1 (these versions work well with GHC 8.0, YMMV).

Next, create a file called blogpost.lagda.md and open it up in Emacs. Here, you write your text using standard markdown syntax. Any Agda code goes between triple backticks:

```
-- write your Agda code here
```

Bonus trick: to hide an Agda code block, just put it between html comments (<!‐‐ and ‐‐>).

You’ll notice that the agda2-mode for emacs is not automatically loaded when editing .lagda.md files. You can either load it manually (using M-x agda2-mode) or fix the problem once and for all by adding this line to your .emacs configuration:

(add-to-list 'auto-mode-alist '("\\.lagda.md\\'" . agda2-mode))

From markdown to html

Once you are finished with writing your blog post, first use Agda to convert the code parts to html:

agda --html --html-highlight=code blogpost.lagda.md

Here, the --html flag tells Agda to generate html from the file, and --html-highlight=code tells Agda not to touch the non-code parts of the file (these will be processed by Pandoc). You should now have a new directory called html containing the following:

To complete the process, run Pandoc on the .md file like so:

pandoc html/blogpost.md -o blogpost.html

This tells Pandoc to convert the markdown file to html (it won’t touch the code since that’s already been converted by Agda).

If you want, you can go wild with any Pandoc extensions you want to use. Personally, I’m just using tex_math_dollars, tex_math_double_backslash and latex_macros (for using LaTeX commands in text).

Integrating with Hakyll

Since I’m building my website with Hakyll, I tried to integrate Agda into the Hakyll pipeline. Unfortunately, this did not go quite as smoothly as I expected: Hakyll is built around the paradigm of mapping one input file to one output file, but this does not match with how agda --html generates its output. For more details on the problem I had, see this post.

Instead, I currently run agda --html on all Agda blog posts as a preprocessing step to Hakyll. This does not work quite as seamlessly as I hoped since Hakyll does not automatically detect changes when running in watch mode, but it gets the job done. If you are also running Hakyll and you want to steal my method, feel free to take a look at it here. Also, if you know of a better method please let me know!

I hope you enjoyed this blogpost about the making of this blog, next time I will finally talk about the long-awaited topic of rewrite rules in Agda (I promise!)