Literate Agda with Hakyll
If you only care about how I did it, you can click here to skip all the rambling!
Introduction
I’ve been playing around with Agda recently to get into dependent types and theorem proving. After making some progress, I wanted to capture my advances and document some concepts. I figured the best way to do this is by making some blog posts! A neat way of documenting code with prose is literate programming. Agda supports various forms of literate programming. I picked Markdown due to familiarity with the syntax.
This blog is statically generated with Hakyll. Under the hood, Pandoc is used to transform the Markdown files into HTML. Markdown Literate Agda (.lagda.md
files) mixes Agda code with Markdown and Pandoc is not able to convert the mix to HTML out of the box. So, I looked for a library that does the conversion and the integration into Hakyll.
Existing Work
I’m obviously not the first person to try this, as both, Hakyll and Agda, are fairly old technologies.
Library hakyll-agda
hakyll-agda
looked promising. It is actively maintained and seemed to provide what I was looking for. However, the lack of documentation made it hard to explore and play around with. The reason I did not opt for this solution is because external Agda libaries, like the standard library, are not explorable in the generated code sections by clicking on them. Maybe I’ve made a mistake in my directory structure that causes this.
Library agda-snippets-hakyll
agda-snippets-hakyll
seemed to have the full functionality that I needed and also had a minimal example on how to use it. However, this library is deprecated in favor of the next approach listed. It also has the upper bound hakyll (<4.10)
, which won’t work with the latest Hakyll version.
Agda Programmatically
Agda is implemented in Haskell and thus provides an interface to programmatically run actions. There is an API to generate HTML for a given Literate Agda file. Both of the aforementioned libraries use this API internally. PLFA, which has been ported to Hakyll, also seems to go this path. This seems to be the cleanest way to do it, but I was not ready to commit too much time to figure and iron out all the intricacies involved. That would mean less time to learn Agda! So, I also did not choose this approach, though, at some point, something like this is the end goal. In hindsight, the Agda Haskell API seems accessible enough to not have to spend too much time getting it to work.
Chosen Approach
Continuing my search for a good enough, satisfactory solution, I stumbled upon this blog post by Jesper Cockx. In the last section of the post, he outlines his method to achieving what I set out to do. He also mentions a problem causing Hakyll’s watch-mode to not work with his approach. The source code is included, which I liberally copy-pasted into my codebase.
To understand his approach and the rest of this blog post, I recommend reading his code. It pretty much calls the agda
executable in Haskell as a process to transform .lagda.md
directly into .html
without calling Pandoc at all. Now there was only the problem of getting the watch-mode to work.
To fix it, I added this route match:
"agda-posts/*.lagda.md" $
match $ do
compile <- getUnderlying
ident $
unsafeCompiler $
processAgdaPost $
takeFileName
toFilePath identmempty :: String) makeItem (
This creates a Compiler a
in an “unsafe” way, meaning it performs an IO
action circumventing the paradigm of mapping one input file to one output file, as described by Jesper Cockx in his blog post.
Upon editing a file matching the pattern, the underlying filename is passed to the processAgdaPost
function, which comes from the aforementioned blog post. This action is executed immediately and an empty Item
is returned. The purpose of this Item
is usually to contruct the one to one correspondence between input and output file. In this case, it is simply a dummy Item
and does nothing. This can be regarded as a bit of a hack, so I’m not fully happy with this solution.
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
You can click on pretty much any non-keyword symbol and you will be taken to the definition. Try clicking on Nat
!
Caveat in the Chosen Approach
If you only add the code snippet above, there is still a problem with synchronization of your agdaInputDir
and the actual site content. Let’s say you remove files from agdaOutputDir
manually and start Hakyll in watch-mode. Hakyll might first run the copyFileCompiler
to copy your .html
from agdaOutputDir
to the site content before it runs processAgdaPost
on all .lagda.md
in agdaInputDir
. In other words, it updates the site content with outdated stuff from agdaOutputDir
and only afterwards is agdaOutputDir
being synced up with agdaInputDir
.
To fix this, I kept the initial processAgdaPosts
call when Hakyll is started. This ensures that the site content is always up to date with agdaInputDir
.
hakyllMain :: IO ()
= do
hakyllMain -- Initial Agda processing
processAgdaPosts$ do
hakyllWith config ...
The catch here is that, in some cases, the HTML generator is run twice in a row. This is very ugly and I plan on fixing it soon by switching to this approach.
There might be another solution, like making the route where the generated HTML is copied to the site content depend on the HTML generation step. This concept seems to be a thing in Hakyll already, but I was not able to get it to work.
Digging Myself a Hole
This section is not relevant to the solution, but I wanted to waffle a bit more about what I did. While the solution above is simple, I struggled quite a bit to find it and, instead, initially went down another path.
At first, I played around with unsafeCompiler
. However, I could not get around the problem, that an Item
had to be returned (the one to one mapping business). I just wanted to run an IO
action.
After digging through the documentation, I found preprocess
. With this function, I could run the HTML generator as a preprocessing step. The problem was that, in watch-mode, this function would run if ANY file was edited. So, editing a file causes the preprocess
step to run, which generates files in agdaOutputDir
. Creating files, just like editing files, causes a rebuild in watch-mode. You might be able to guess what happens now: preprocess
is being run AGAIN, causing an infinite loop. I was not able to avoid this infinite loop with the API that Hakyll provided at the time. So, I changed Hakyll’s API.
I opened an issue to allow certain directories to be ignored in watch-mode. This would allow me to ignore changes in agdaOutputDir
, so preprocess
could generate HTML freely into that directory without triggering a rebuild. After some back and forth, Minoru (a Hakyll maintainer, big thanks to them!) and I agreed on an API. I added a new field to the Configuration
record taking a predicate. This predicate is called if a file is edited/created with the file path (relative to where Hakyll is being run). Something like this:
config :: Configuration
=
config
defaultConfiguration= ("_agda/**" ?==)
{ watchIgnore }
If a file is now generated/edited in the _agda
directory, this predicate will return True
, making the watch-mode ignore it and not trigger a rebuild. ?==
comes from filepattern
.
This fixes the problem with preprocess
, but it was a lot of effort for a solution I was not content with. Every file change still triggered the agda
process, causing unnecessary rebuilds.
Then it dawned on me that I could make the unsafeCompiler
version work by just returning an empty item. I did exactly that, was surprised it was so easy and realized my API change was not necessary to solve my problem. This open-source contribution to Hakyll was a nice little side effect of me digging a hole when I should’ve just taken a few steps back and re-evaluated my options. Oh well 🤷♂️.
Update 12.10.2021
Fixed some typos, improved explanations.