Skip to content
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

Open
Kha opened this issue Oct 7, 2021 · 9 comments
Open

RFC: reorganizing docs #717

Kha opened this issue Oct 7, 2021 · 9 comments
Labels
documentation Documentation improvement

Comments

@Kha
Copy link
Member

Kha commented Oct 7, 2021

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:

@leodemoura
Copy link
Member

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

@Kha
Copy link
Member Author

Kha commented Oct 7, 2021

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.

@PatrickMassot
Copy link
Contributor

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.

@lovettchris
Copy link
Contributor

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/

@Kha
Copy link
Member Author

Kha commented Oct 7, 2021

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.

@kim-em
Copy link
Collaborator

kim-em commented Oct 8, 2021

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

@XVilka
Copy link

XVilka commented Oct 11, 2021

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.

@leodemoura
Copy link
Member

@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 leodemoura added the documentation Documentation improvement label Jun 1, 2022
@Kha
Copy link
Member Author

Kha commented Jun 2, 2022

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.

ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
* Remove instance and add `to_additive`
* Point some comments to the right issue
* Resolves the issue in leanprover#707
* Might conflict with leanprover#717
ChrisHughes24 pushed a commit to ChrisHughes24/lean4 that referenced this issue Dec 2, 2022
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]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Documentation improvement
Projects
None yet
Development

No branches or pull requests

6 participants