doc-strings and descriptions for options

Stream: lean4

[Eric Wieser]

Where can I read what set_option backward.whnf.reducibleClassField false means? I can't tell from the docstring which setting is true and which is false, nor what the default is!

[Thomas Murrills]

The docstring on the option declaration itself may be more helpful (the hover shows the descr):

When true, unfolding a [reducible] class field at TransparencyMode.reducible also unfolds the associated instance projection at TransparencyMode.instances.

Motivation: Consider a ≤ b where a b : Nat and LE.le is [reducible]. Unfolding LE.le gives instLENat.1 a b, which is stuck because instLENat is [implicit_reducible] (not [reducible]). Similarly, stM m (ExceptT ε m) α unfolds to an instance projection that is stuck at .reducible. Without this option, marking a class field as [reducible] is pointless when the instance providing it is only [implicit_reducible]. This option makes the [reducible] annotation on class fields work as the user expects by temporarily bumping to .instances for the projection.

See unfoldDefault for the implementation.

(the default value seems to be true? I don't believe it's overridden in mathlib's lakefile)

[Eric Wieser]

I've always found it a bit weird how there are both docstrings and descrs for options; was there ever discussion about merging them?

[Thomas Murrills]

(We should move this discussion to a new topic :grinning_face_with_smiling_eyes:) I'd be in favor of merging them! I've never understood the reason they're separate either.

[Notification Bot]

4 messages were moved here from #mathlib reviewers > requests for speedy review/delegation by Kim Morrison.

[Thomas Murrills]

Interestingly, the server first looks for a docstring, then falls back to the descr. This means that you have the full docstring as hover in the following, but you lose it if you comment out import Lean:

import Lean -- comment out

set_option backward.whnf.reducibleClassField true

This seems a bit inconsistent...it would be nice to have the same hover everywhere! At first I thought this might also be an issue for non-core options due to module system changes, but there's actually a different issue there: #lean4 > Language server allows `set_option`s that `lake` doesn't

However, the descr is also used for preview text during autocomplete (and the docstring isn't). Maybe that's its true role? It makes sense for that to be more minimal.

I would be in favor of making sure the hover is the same everywhere for builtin options somehow, if it's not an insurmountable technical challenge, and clarifying that the descr field is only intended for "what is seen in autocomplete hints", if true.