[Agda] Agda Tutorial darcs repo & pandoc backend
Peter Divianszky
divipp at gmail.com
Wed Jan 23 15:14:46 CET 2013
Hi,
I have made a darcs repository for the tutorial I presented at AIMXVI.
http://hub.darcs.net/divip/AgdaTutorial
You can look at the HTML version at
https://people.inf.elte.hu/divip/AgdaTutorial/Index.html
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:
http://hub.darcs.net/divip/AgdaTutorial/browse/Agda.patch
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?
Cheers,
Peter
More information about the Agda
mailing list