RFC: docstrings on trace options

[nomeata]

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 :+1: to issues you consider important. If others benefit from the changes in this proposal being added, please ask them to add :+1: to it.

[Kha]

A separate command would be nice in that we could also use it to make trace classes first-class values, as in https://github.com/leanprover-community/aesop/blob/master/Aesop/Tracing.lean

[semorrison]

The branch trace_descr contains work in progress on this, although I'm balked at the moment by stage0 problems.