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:
- The Agda files must be top level modules.
- An Agda interface file will be generated along the original literate file, so you must tell Hakyll to ignore said interface files (which end in
- Hakyll metadata is not “filtered out”, so it’s better to include it as a separate
- Only links internal to the file will be generated. Cross links between blog posts of the same site could easily be achieved.
- The generated code is in a
pre.Agdablock. A css file (
css/agda.css) adapted from the one distributed with Agda, is provided in the package.
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.