Thoughts on literate programming tools


TL;DR: I’m thinking about a next-generation literate programming tool, and I want to improve the “woven” part, say, documentation generation (particularly, HTML).

I have contributed to the HTML backend of literate Agda, and have made several similar tools (generate clickable and highlighted HTML) in both IntelliJ-Pest and IntelliJ-DTLC.


If you have followed me on Twitter, you may have seen my recent shitposts on a markup language. The motivation was to create a blog about programming/theorem proving in the Arend programming language, which requires a literate programming tool. Markdown with codeblocks may work, but that’s too weak – even literate Agda supports dumping highlighting and navigation for references (say, the variables in code blocks are clickable and they jumps you to their definitions), and the two highlighting engines used by Jekyll (the default blog renderer used by GitHub Pages), Rouge and Pygments, neither support Arend syntax highlighting.

Also, the official website of Arend uses a Jekyll plugin to highlight Arend code – and it’s token-based.

Providing all these banes and pains, why not create my own literate mode for Arend then? I can do whatever I want in my own tool – there’s a broad space for us.


So, since I’m already creating a my own literate mode, why not create my own markup language? Markdown is already millions behind AsciiDoc and reStructuredText, but we’re aiming a even more powerful literate programming tool, so I consider a brand new markup language necessary.

I think I need to rely highly on compiler integration, say, users will probably need to add some very complicated plugins to the markup language compiler in order to support their own programming language. Well, at the very first stage, I’ll support Arend only because I am aware how complicated a plugin system is :)

Since Arend it written in Java, my markup language will probably be in Java or Kotlin.


First, I need to make an Arend-to-HTML generator, so I can have references to an external file (since there’s Prelude.ard). This should be easily done, and I may add it to the compiler as an extra functionality directly.

Here’s some ideas come into my mind (the following content is similar but different from my tweets):

So, what’s the actual syntax and markup features it’ll support?

Well, I’m still thinking about it. I talked to Oling Cat and KiWA, but none of which seem to be passionate about the idea. Probably I can only design it myself, and let potential users suffer from my personal taste, which is often weird :(

Tweet this Top


This work (Thoughts on literate programming tools) is licensed under a Creative Commons Attribution-NonCommercial-NoDerivatives 4.0 International License.