Generating documentation?

Stream: lean4

[Siddharth Bhat]

I'm quite envious of the Lean3 mathlib documentation. I gather this was generated using doc-gen. Is there a port of this to Lean4?

[Henrik Böving]

Im working on it! https://github.com/hargoniX/doc-gen4/.

[Siddharth Bhat]

Need some help? [Is it feature-complete? I'd be happy to work on things if there's a pointer to what needs to be done!] :)

[Henrik Böving]

It's very far from being feature complete :sweat_smile: right now there is the part that fetches at least large chunks of the information we need from the compiler internals (this is happening mostly in Process.lean) and what I'm currently sitting on is basically porting all the templates from the original doc-gen over to the new one (instead of jinja2 we have a JSX like DSL which I got from an abandoned PR to the compiler). It is currently capable of doing the index page + this navbar at the side (in Output.lean) but all the pages have to be filled with content still^^

[Arthur Paulino]

Siddharth Bhat said:

Need some help? [Is it feature-complete? I'd be happy to work on things if there's a pointer to what needs to be done!] :)

Looking at doc-gen issue tracker, the features that draw most of my attention are related to searches. Maybe #104 in particular? IDK.

Take a look at those issues and see what interests you the most and check with the community what ppl think :D

[Henrik Böving]

Oh if its about sparkly new features users have asked for there was a doc-gen4 thread somewhere below where people listed lots of stuff they'd want to see in the new doc-gen.