lean2md

Stream: general

[Arthur Paulino]

I made this Python script and I thought that other people might find it useful. So I made a package with it and hosted it on PyPI.

It creates markdown files from Lean files. If you have a directory with a bunch of Lean files and want to create md files out of them to make a blog post or a mdbook, you can use it.

It's nowhere nearly as powerful as Alectryon, but it gets the job done with a reasonably small effort and simplified API.

https://github.com/arthurpaulino/lean2md

[Clément]

Very nice! Note that the part of Alectryon that flips comments around is a single file, with its own CLI and no dependencies on the rest of the software, so you can use alectryon/literate.py directly if you're not interested in the rendering. Even then your solution is very neat and short (Alectryon's implementation spends a lot of effort on the reverse direction, which needs to keep track of things like indentation :'(, nested comments, and positions, which makes it much longer and less pleasant to debug)