RFC: Separate out doc.verso option between module docs and declaration docs #12070
Description
Proposal
This RFC proposes a doc.verso.module option that controls whether the current file's module docs (between /-! -/) are parsed as Verso or not, and does not influence parsing of declaration docstrings (between /-- -/). This is intended to simplify incremental porting of docstrings to Verso.
Module docstrings currently do not support set_option verso.doc _ in, since all module docs need to have a consistent syntax (either Verso or plaintext/markdown). Enabling set_option verso.doc _ in for module docs does not seem a practical solution, it would be very hard to implement mixing of the two formats. This means with the current setup, enabling Verso for module docs will need explicitly keeping track of the doc.verso state:
section VersoIncompatible
set_option doc.verso false
/-- This docstring is not yet ported to verso. -/
def foo0 := 1
set_option doc.verso true
/-! Nicely formatted module docs ... -/
set_option doc.verso false
/-- This docstring is not yet ported to verso. -/
def foo1 := 1
/-- This docstring is not yet ported to verso. -/
def foo2 := 1
...
end VersoIncompatible
section VersoCompatible
set_option doc.verso true
/-- This docstring is already ported to verso. -/
def bar0 := 1
-- No `set_option doc.verso true`, because the docstrings in this section are already ported.
/-! Some more nicely formatted module docs ... -/
-- No `set_option doc.verso false`, because the docstrings in this section are already ported.
/-- This docstring is already ported to verso. -/
def bar1 := 1
/-- This docstring is already ported to verso. -/
def bar2 := 1
...
end VersoCompatibleHaving to surround all module docs with (up to) two lines of set_option makes it easy to miss out a set_option or add one too many and silently turn off Verso. (And subjectively, it looks ugly).
It would be impractical to port all of Mathlib's module docstrings at once, so some measure is needed to provide incrementality. Per-file incrementality on the module doc level is doable.
Therefore, I would like to be able to write instead:
set_option doc.verso.module true
section VersoIncompatible
set_option doc.verso false
/-- This docstring is not yet ported to verso. -/
def foo0 := 1
/-! Nicely formatted module docs ... -/
/-- This docstring is not yet ported to verso. -/
def foo1 := 1
/-- This docstring is not yet ported to verso. -/
def foo2 := 1
...
end VersoIncompatible
section VersoCompatible
set_option doc.verso true
/-- This docstring is already ported to verso. -/
def bar0 := 1
/-! Some more nicely formatted module docs ... -/
/-- This docstring is already ported to verso. -/
def bar1 := 1
/-- This docstring is already ported to verso. -/
def bar2 := 1
...
end VersoCompatibleSpecifically: if doc.verso.module is set to true, module docs are parsed as Verso. If doc.verso.module is set to false, module docs are parsed as plaintext/Markdown. And this will happen regardless of the value of doc.verso, enabling the full truth table of doc.verso and doc.verso.module to be expressed. (For Mathlib it might also be acceptable to have doc.verso true always imply module docs are parsed as Verso, regardless of the setting of doc.verso.module. But I do not see a strong advantage for this behaviour.)
If the option doc.verso.module is not explicitly set, it should fallback to the value of doc.verso: this replicates current behaviour. And it provides a method for removing the set_option lines when doc.verso gets enabled globally in Mathlib. Having the default value of doc.verso.module depend on the value of doc.verso does mean that setting doc.verso can unintentionally affect doc.verso.module if that is still unset. In the cases where that is undesirable, the user can also set doc.verso.module to their desired value immediately afterwards.
Community Feedback
Incremental porting is a required feature for Mathlib making use of Verso, as discussed with Mathlib Initiative colleagues. The specifics of how to incrementally port module docs were clarified together with David Thrane Christiansen on Zulip.
Impact
Add 👍 to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add 👍 to it.