lean4 icon indicating copy to clipboard operation
lean4 copied to clipboard

RFC: reorganizing docs

Open Kha opened this issue 3 years ago • 9 comments

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/

Kha avatar Oct 07 '21 11:10 Kha

I think this is a good idea. Should we use separate repos?

leodemoura avatar Oct 07 '21 13:10 leodemoura

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.

Kha avatar Oct 07 '21 13:10 Kha

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.

PatrickMassot avatar Oct 07 '21 16:10 PatrickMassot

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/

lovettchris avatar Oct 07 '21 20:10 lovettchris

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.

Kha avatar Oct 07 '21 20:10 Kha

It's early days yet --- I'd just break the existing URLs rather than have to carry along a hack forever.

kim-em avatar Oct 08 '21 00:10 kim-em

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.

XVilka avatar Oct 11 '21 04:10 XVilka

@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?

leodemoura avatar Jun 01 '22 23:06 leodemoura

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.

Kha avatar Jun 02 '22 08:06 Kha