[Agda] Agda Tutorial darcs repo & pandoc backend

Peter Divianszky divipp at gmail.com
Wed Jan 23 15:14:46 CET 2013


I have made a darcs repository for the tutorial I presented at AIMXVI.


You can look at the HTML version at


I plan to successively improve this tutorial.

All the HTML files are generated from literate Agda files with a 
modified Agda compiler which uses pandoc for HTML generation.

You can find the patch for the Agda compiler here:


I plan to improve the patch in the following ways (both are easy as 
pandoc has support for these):

-   make HTML slide generation working
-   proper handling of LaTeX code inside markdown comments

With the following improvements pandoc could be a general
solution for static presentation of Agda code:

-   allow multiple output formats
-   allow multiple input formats
-   process comments in code too, not just around code blocks
-   process code comments in comments as Agda code

On the other hand, pandoc dependencies are too much for the Agda compiler.
Maybe conditional compilation could solve this.
What do you think?



More information about the Agda mailing list