-
Notifications
You must be signed in to change notification settings - Fork 458
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
RFC: reorganizing docs #717
Comments
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 |
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: 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. |
* Remove instance and add `to_additive` * Point some comments to the right issue * Resolves the issue in leanprover#707 * Might conflict with leanprover#717
mathlib SHA e50b8c261b0a000b806ec0e1356b41945eda61f7 This completes an earlier partial port of the file. ~~I added a workaround for the issue explained by Floris at leanprover-community/mathlib4#707 (comment) Co-authored-by: Ruben Van de Velde <[email protected]>
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
This mostly mirrors Rust's documentation structure:
The text was updated successfully, but these errors were encountered: