request: config file to set repo-specific information

[hrmacbeth]

If I understand correctly, certain fields that one might want to set in the documentation on a repo-by-repo basis are currently hard-coded in doc-gen4. For example,

• the title displayed in the top left corner (hard-coded as "Documentation", mathlib3 docs say "mathlib documentation" with a link on "mathlib" to the leanprover-community website)
• the central panel of the index page (hard-coded as "What is up?" :smiley:), mathlib3 docs have several paragraphs introducing mathlib and giving links to the mathlib, Lean-fork and doc-gen versions that the build is based on
• the HTML <title> tag (hard-coded as eg "Mathlib.Algebra.Group.Basic", mathlib3 docs say "algebra.group.basic -- mathlib docs")

What would be the best way to allow this to be set on a repo-by-repo basis? Maybe a fixed format for a configuration file which could live in the top level of the associated repository?

(Note: maybe with that method it wouldn't be possible to have these fields to contain links to the mathlib/Lean/doc-gen commits used to generate the docs, the way that the central index panel does in the mathlib3 docs. So maybe we should also find another place to display that information.)

[hargoniX]

We do already have a CMark API for Lean 4 right now which would allow us to render user provided markdown files into HTML and present it as the index page. In general it might be interesting to have some sort of templating language like say jinja2 integrated with Lean both for doc-gen and maybe other programming related purposes in the future.