Deep terms ellipses

Stream: lean4

[Patrick Massot]

I am not a fan of the new … that appear in “deeply nested” expressions. The issue is that it seems to use a definition of depth that is not the relevant one, at least for mathematics. In a + b + c + d, all letters are at the same depth for mathematicians. More generally, a function taking several (explicit) arguments has all its arguments at the same depth in general. This is very different from a (b (c d)). If we can’t agree on this, could the elision be opt-in? At the very least, can the popup you get when clicking on … mention how to configure the depth that is showed? And is there an option you can put in the lakefile to set the default depth for the project?

[Marc Huisinga]

Do you have an MWE where you see the ellipses for a non-proof-term? pp.deepTerms is true by default, so deep terms should not be omitted by default.

[Patrick Massot]

Actually I was confused, the example I saw yesterday was indeed a proof. But I was misled by the example showed during the FRO meeting.

[Mario Carneiro]

I think this is a performance optimization, if you see any ... at all then you should interpret this as lean trying not to run out of memory or take too long while processing your request. Unfortunately this doesn't necessarily match the "mathematical" notion of depth, and using that definition could still cause the same issues, i.e. if your goal is that a sequence of 10000 terms added together is equal to something then this will cause something to break in lean and/or vscode even though the "mathematical depth" is small

[Kyle Miller]

I'm not sure why the hover isn't showing the docstring for the omission symbol. This is what you're supposed to see:

Denotes a term that was omitted by the pretty printer. This is only meant to be used for pretty printing, however for copy/paste friendliness it elaborates like _ while logging a warning. The presence of ⋯ in pretty printer output is controlled by the pp.deepTerms and pp.proofs options.

[Kyle Miller]

Oh right, this is why:

| .ofOmissionInfo _ => return none -- Do not display the docstring of ⋯ for omitted terms

[Kyle Miller]

@Patrick Massot Here's a PR to show the docstring for the omission symbol on hover: lean4#3663

image.png

Does this explain ⋯ satisfactorily now?

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

It's potentially still a bit confusing to show the expanded term and the docstring for ⋯ under it, since normally it'd be the docstring for the term. But maybe it's clear enough from context.

[Kyle Miller]

I'd say it's confusing, but it's better to have this information than not have it.

Maybe the docstring should mention that it's for ⋯ in the first couple words?

[Kyle Miller]

Maybe this is a little less confusing?

image.png

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Yup, that's quite clear!

[Kyle Miller]

I'm curious, what would it take to be able to have brief and full docstrings for the hovers? The way it would work is that when you initially hover, you get the brief docstring, and if you either click on an "expand"-type button (or maybe wait long enough), you get the full docstring?

An encoding hack would be to use html comments to indicate a point in the docstring, where everything before it is the brief docstring, like this:

/--
The `⋯` term denotes a term that was omitted by the pretty printer.<!--brief-->
The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options,
and these options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`.

It is only meant to be used for pretty printing.
However, in case it is copied and pasted from the Infoview, `⋯` logs a warning and elaborates like `_`.
-/
@[builtin_term_parser] def omission := leading_parser
  "⋯"

The reason why hovering over ⋯ doesn't show the docstring at all is that it's mostly noise that just increases the size of the hover box. You get the idea of what ⋯ is pretty quickly, so you don't need the full docstring.

This applies to many other hovers too. One that comes to mind is hovering over =, which at some point you don't feel like you need a full explanation of it anymore :-)

[Patrick Massot]

That would be really nice.

[Yaël Dillies]

FWIW I've trying to write all my docstrings in the

/-- Short docstring.

Longer docstring. -/

style for the past few months.