RFC: docstrings on trace options

Proposal

Currently, the docstring when overing on

set_option trace.Elab.command true
set_option trace.Elab.syntax true
…

always says

enable/disable tracing for the given module and submodules

hardcoded in

def registerTraceClass (traceClassName : Name) (inherited := false) (ref : Name := by exact decl_name%) : IO Unit := do
  let optionName := `trace ++ traceClassName
  registerOption optionName {
    declName := ref
    group := "trace"
    defValue := false
    descr := "enable/disable tracing for the given module and submodules"
  }
  if inherited then
    inheritedTraceOptions.modify (·.insert optionName)

It seems the original design for trace option was that they would just indicate a module trace.Elab.Foo, but it seems in practice we have all kinds of trace options with interesting semantics that deserve to be described, so that I see what these options do in the auto-completion or hover tooltip.

An optional parameter to registerTraceClass might do. Or, more fancy, a command for

builtin_initialize
  registerTraceClass …

whose docstring is then moved to the option.

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.

Start with the registerTraceClass function shown in the issue and inspect how trace options provide descriptions to auto-completion and hover tooltips. Determine whether an optional parameter or a builtin_initialize command best fits the existing registration path; done means trace options expose semantics-specific docstrings instead of the hardcoded description.