lean4
lean4 copied to clipboard
RFC: reorganizing docs
There have been multiple discussions about the structure of our documentation recently. There is also a practical issue of the chapter sidebar becoming too long to comfortably navigate the mdBook without missing that there are completely separate parts hidden in there.
Thus I'm proposing to split the documentation into multiple separate books, something like
- Language Manual: explaining the 80% of the language above the waterline using small examples
- Reference Manual: the gnarly details, forever incomplete from experience
- Tutorials: documents focusing on single, bigger examples, (mostly?) contributed by external people, but maintained by us
- Development Manual: what pure users don't need to know
This mostly mirrors Rust's documentation structure:
- https://doc.rust-lang.org/book/
- https://doc.rust-lang.org/reference/ (including incompleteness :sweat_smile: )
- https://doc.rust-lang.org/stable/rust-by-example/
- https://doc.rust-lang.org/rustc/
I think this is a good idea. Should we use separate repos?
I don't think that's necessary unless we expect many external contributions, and it would complicate CI-testing the code blocks. Separate folders with separate mdbook configurations should be sufficient.
I guess you already know this, but just in case, it seems that https://documentation.divio.com/ has interesting ideas about splitting documentation. Maybe it could be one source of inspiration.
so long as there is still one website hosted by github then one repo is fine. If you are talking about different top level websites, they will need to be different repos because of the way github pages works.
I totally agree there are 4 different kinds of documentation and we need all of them. "tutorials, how-to guides, technical reference and explanation". My previous project has pretty much exactly this structure hosted in one github pages site: See https://microsoft.github.io/coyote/
Oh, I don't think there's any reason not to host all of them in doc/
. Speaking of URLs though, should we try to keep the current URLs valid? Redirections can only be done hackily in GitHub pages unfortunately, but breaking all the current URLs also feels wrong.
It's early days yet --- I'd just break the existing URLs rather than have to carry along a hack forever.
I also suggest to consider the switch from the mdBook in the long run, since it's doesn't support PDF and ePub generation, and there are no plans or any activity from their developers to do so:
- https://github.com/rust-lang/mdBook/issues/88
- https://github.com/rust-lang/mdBook/issues/815
We (Rizin) recently did the switch from the mdBook to pandoc-based Quarto.
The amount of changes to migrate was relatively small, and it's much more feature-complete than the mdBook, just see their gallery.
@Kha I am happy to address this issue in the next following weeks. This issue was created a long time ago, did you change your mind, and/or have new ideas?
I think the only relevant change since then is that our ToC now has a more reasonable size thanks to collapsing subsections, which may avoid the need for separate books. As well as continuing discussions about whether we should move away from mdBook.