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:
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.