doc: describe the sidebar components (Aesop, Init, Lake, Lean, Mathlib, etc) and where their code is located

[hargoniX]

doc-gen4 (unlike the original) does not intend to be a tool that is only used within the mathlib eco system. People that build their own mathlib independent (or mathlib extending) eco systems should be able to do that just like that.

Because of this a text like this is not included currently and I also wouldn't like to include one that statically refers to some part of the eco system. Also note that all declarations already have a source link available to click.

The correct solution if we wish to extend the index is (IMO) to provide users with an ability to supply a markdown file (or in the future: A file in the format that David is working on) which gets rendered into the index.

[hmonroe]

Understood, but it seems that a bullet/blurb is needed for each source, which can be combined into a list. Or more simply a toggle to include my language only for mathlib. I can work on something if there is an agreed approach.

[hargoniX]

Understood, but it seems that a bullet/blurb is needed for each source, which can be combined into a list. Or more simply a toggle to include my language only for mathlib. I can work on something if there is an agreed approach.

I think there is a misunderstanding here? I do not intend for mathlib specific code to end up in doc-gen, also not as a switch, toggle etc. There shouln't be any features that are available to mathlib but not to other libraries that exist in the Lean universe.

To extend on my last comment, if people wish to have a custom index the way to go is IMO as follows:

1. Decide on some location for a markdown file, lets say docs/doc-gen-index.md or dcindex.md, doesn't really matter in the end.
2. Add code in the index renderer that checks whether this file is available and if it is uses the CMark dependency (already used for rendering doc-strings) to turn that file into HTML. Note that it should be possible to have a repo without this file still so people can just use doc-gen out of the box without any additional work.
3. Put that HTML into the generated index.html page
4. Add such a file to mathlib (or any other library) to get a custom index.

[hmonroe]

OK, so for Lean 4 itself, the file doc-gen-index.md would consist of: "Init is the initial code loaded by Lean 4 and is maintained in the github repository https://github.com/leanprover/lean4. Std is the standard library distributed with Lean 4 and is maintained in the github repository https://github.com/leanprover/std4." Or perhaps in two files in the two repositories.

Am I right that doc-gen4 has not been used to generate output posted somewhere for Lean 4 alone and not with mathlib4? And that the Lean 4 documentation, web page, and the book Functional Programming in Lean 4 do not refer anywhere to doc-gen4 output?

[hargoniX]

Am I right that doc-gen4 has not been used to generate output posted somewhere for Lean 4 alone and not with mathlib4?

yes

And that the Lean 4 documentation, web page, and the book Functional Programming in Lean 4 do not refer anywhere to doc-gen4 output?

I do not know.

OK, so for Lean 4 itself, the file doc-gen-index.md would consist of: "Init is the initial code loaded by Lean 4 and is maintained in the github repository https://github.com/leanprover/lean4. Std is the standard library distributed with Lean 4 and is maintained in the github repository https://github.com/leanprover/std4." Or perhaps in two files in the two repositories.

I wouldn't overcomplicate it so much for now. Once such a feature is implemented I'd suggest to just put a file with your text in the mathlib4 repo. doc-gen just renders that file (and none from other repos) when it is called for that repo. If the other libraries wish to have other, possibly long introductory texts they can do that in their own renders as well.

Long time the vision is to have doc-gen be used in a more https://docs.rs fashion where the libraries are hosted centrally and you dont generate one large doc blob for the entire transitive closure of your lib but instead just your library alone and the rest gets automatically linked to other libraries on that hypothetical future website.

[acmepjz]

Maybe there should be a feature which let each module provide a short description of it, and then the doc-gen4 gather all of them to the front page. Not hard-coded one.

[acmepjz]

I think this is related to #43.