autocomplete help for options

Stream: mathlib4

[Bhavik Mehta]

When I start typing a trace option and I use autocomplete to see what choices I have, the autocomplete suggestions come with relatively unhelpful information. Is there a way we can put some more relevant information here?
image.png
Each of the options above give the same text, except for switching true/false. Ideally I'd want something like a function docstring which gives me some idea of what the options do

[Alex J. Best]

https://github.com/leanprover/lean4/blob/634f6963cf508345862f8e8a32f0afa03eb80e5a/src/Lean/Util/Trace.lean#L224 is your culprit. You'll have to open a core RFC to get that improved I guess.
Aesop has its own way of doing this https://github.com/leanprover-community/aesop/blob/bf5ab42a58e71de7ebad399ce3f90d29aae7fca9/Aesop/Tracing.lean#L20C4-L20C4 that we could adopt in mathlib I suppose. But seeing as many of the interesting traces are defined in core I see no way to add information there after the fact

[Scott Morrison]

Ideally we would just write a doc-string on the initialize registerTraceClass ... line, but I don't see any way to tunnel that information through to the descr field.

[Scott Morrison]

Unless there is a trick like by exact decl_name% but that can grab the current declarations doc-string? That doesn't sound so implausible.

[Scott Morrison]

Then we would just add an optional argument to registerTraceClass.

[Scott Morrison]

If there's no by exact decl_name% available, we could have a macro that grabs /-- XYZ -/ initialize registerTraceClass and feeds XYZ in as an additional argument??

[Mario Carneiro]

I have definitely written code to steal the docstring from the initialize declaration using decl_name% before for something

[Mario Carneiro]

the doc isn't even correct, it says enable/disable tracing for the given module and submodules but the docstring on registerTraceClass says By default, trace classes are not inherited

[Mario Carneiro]

I kind of want to just get rid of manual setting of the descr field altogether. It encourages single line docs because it's a string literal

[Eric Wieser]

Is it time to bring back /-" comment strings "-/?

[Scott Morrison]

Mario Carneiro said:

I have definitely written code to steal the docstring from the initialize declaration using decl_name% before for something

I've you remember where, I'm happy to crib.

[Scott Morrison]

I agree the descr field is very unhelpful.

[Mario Carneiro]

Looking into it more, I'm leaning more toward something more like what the lake package et al macros do, and just take over elaboration of the structure literal in register_option, so that the macro can take the doc string and put it in as descr

[Damiano Testa]

If it were possible to rewrite doc-strings after the fact, that would also solve this issue.