Can I render my Lean as HTML?

Stream: Is there code for X?

[Nicholas Dyson]

Theorem provers can (I am aware that Coq does, at least) have associated tools that convert a source file into a pretty HTML document usable for showing the results. Does such a tool exist for Lean? I was able to find this (https://github.com/leanprover-community/format_lean) link, but it hasn't been updated in a year and I can't get it to work - it errors even on an absolutely minimal file containing nothing but a proof that x = x.
Is there a more up-to-date alternative?

[Eric Wieser]

I assume doc-gen doesn't do what you're after?

[Johan Commelin]

@Patrick Massot is our expert here. But roughly, I think we just lack the people power right now to build these tools. Even though we would love to have more tools in this direction.

[Eric Wieser]

(it shows results but not proofs)

[Patrick Massot]

format_lean hasn't been updated because it just works for its intended purpose last time I checked.

[Patrick Massot]

For instance this page is using it (there is Lean code at the bottom).

[Patrick Massot]

But it's a pretty rudimentary tool, we are waiting to find man power to port Alectryon.

[Nicholas Dyson]

Thanks for the advice, I wasn't aware of doc-gen. I can probably use that to do most of what I need.

[Eric Wieser]

While doc-gen is very much built for mathlib only, it's not too hard to tweak it to run on other projects