mdgen: lean2md in pure lean

Stream: general

[Asei Inoue]

I find lean2md a very useful tool and I like it a lot. However, lean2md is written in Python, so I needed to install Python to use it, and I wanted to rewrite it purely in Lean.

Also, some parts of lean2md are not flexible since it is already used in the metaprogramming book. I wanted to add some features for my own use.

So I re-implemented lean2md in lean.

https://github.com/Seasawher/mdgen

[Patrick Massot]

That's nice but you should have asked about existing plans. @David Thrane Christiansen is working on a much more powerful tool that will soon make lean2md completely obsolete.

[Arthur Paulino]

But it's available now rather than soon. And its simplicity has its own appeal (roughly 100 lines of code).

@Asei Inoue if you want, you can adapt the metaprogramming book to use it instead of lean2md so Python would no longer be needed to generate the md files

[Asei Inoue]

@Patrick Massot That's nice. By "much more powerful", what new features are you referring to?

[Asei Inoue]

@Arthur Paulino I am interested in replacing lean2md in metaprogramming. mdgen converts not only files in directories, but also child directories, so the commands should be more concise.

[Asei Inoue]

But mdgen also support doc comment. This feature is same as suggested in https://github.com/arthurpaulino/lean2md/pull/4 , which breaks the metaprogramming book.
Therefore, we may need to change the lean file in the metaprogramming book. I think It is better not to touch the lean file itself.

[Arthur Paulino]

Right, that's the annoying part of what I meant by "adapting the metaprogramming book". If the Lean files can be adjusted to produce the same output using mdgen as it's meant to be used, that would be preferable

[Patrick Massot]

Asei Inoue said:

Patrick Massot That's nice. By "much more powerful", what new features are you referring to?

A whole world of new features. This is a totally different scale project. You will learn a lot more during David's talk next week.

[David Thrane Christiansen]

It's not exactly a secret - I'm working on representing documents as a DSL in Lean. The concrete syntax is mostly Markdown, but the document itself is a normal Lean value. This is to provide the tools needed to assemble lots of different document workflows, from blog posts to software documentation to blueprints to research papers, with lots of opportunities for code reuse but without shoe-horning them into a single limited model. I plan to develop tools for software manuals, online didactic books, and software documentation at the very least, and I want to support others in building their own instantiations for other purposes.

That said - I want people to use this project if and when it meets their needs, and I hope it doesn't stifle other innovation or keep people from having fun and doing their own thing. And while I'm making good progress, it's not yet ready to take over for all our various books.

But yes - more in the talk next week!

[David Thrane Christiansen]

The main inspirations are Scribble and Sphinx

[Asei Inoue]

@David Thrane Christiansen I'm looking forward to it!

@Arthur Paulino It seems that the lean version of the metaprogramming book is too old to install mdgen.

[Arthur Paulino]

Makes sense. In that case, it probably requires a toolchain bump. If the metaprogramming API hasn't changed too much, it shouldn't be too much of a problem

[Asei Inoue]

deleted

[Asei Inoue]

@Arthur Paulino I submitted a pull request. https://github.com/leanprover-community/lean4-metaprogramming-book/pull/123

[Arthur Paulino]

I've asked @Julian Berman to follow up and he accepted, which is nice because he has more context on the CI flow. I'm going to be away from my computer for the next 24~48h.

Thank you both!