2013-04-19 Literate Agda and Hakyll

To render nicely my previous post I have written some glue Haskell code that implements an Hakyll Compiler that supports Agda files. The interesting function is pandocAgdaCompilerWith. It takes configurations for the Pandoc reader and writer and for the Agda compiler and produces HTML files. The HTML is produced by interpreting the non-code in the literate file as Markdown.

The code works but has some rough edges:

An example of the package in action can be found in the Haskell code that generates this website, where site.hs is the main generator and posts/AgdaSort.lagda (and the respective metadata file) is a literate Agda file that generates the post mentioned before.