Status of the Mathlib Manual

Stream: mathlib4

[Niels Voss]

What sort of info is designed to end up in the Mathlib Manual https://leanprover-community.github.io/mathlib-manual/html-multi/? Is it open for contributions? How should we decide whether to put info in a docstring, a library note, the leanprover-community website, Mathematics in Lean, or the mathlib manual?

Which of the following things would be on topic for the Mathlib manual, and which would be better fit elsewhere or not a good idea at all?

• Toolchain setup tutorials (e.g. how to fix a broken lake install, how to build a local copy of the docs, how to set up local loogle, how to add extra contributor only dependencies like lean-hammer or canonical to a local version of mathlib)
• Bird's eye views of mathlib, like how the algebraic hierarchy fits together, the layout of folders in mathlib, and what stuff is on topic for mathlib?
• Overview of a particular subtopic that are too general to fit as a docstring for a single file (e.g. what all the main topology typeclasses are, what properties a topological space might have, how to convert between linear maps and matricies etc.)
• General natural language math exposition for concepts that most mathematicians either haven't learned or haven't learned at the level of generality Mathlib uses, and might have difficulty understanding the mathematical background behind mathlib (e.g. tutorial on filters and ultrafilters, tutorial on uniform spaces, induced and coinduced topologies and how those correspond to the quotient and subspace topologies, etc.)
• Explanations of how to express informal math statements in Lean, like "To state 'let X be a vector space over a field K', write variable (K : Type*) (X : Type*) [Field K] [AddCommGroup E] [Module K E]"
• Contributor guides (e.g. naming conventions, how deprecations work, code style policies)

[Kim Morrison]

Is there some previous zulip discussion of this, that someone can link to?