Improve UX for long instance names

[utensil]

For now, Lean generates long instance names for anonymous instances like this:

The historical reasons and improvements suggestion can be found at lean4#2343 and mathlib4 > instance names on Zulip.

The takeaway seems to be that it's for avoiding name clash, and it's unlikely to change until a consensus on the new name scheme is settled.

@Kha (Sebastian Ullrich) suggests and got upvoted:

As "naming things" famously is one of the hardest problems of CS and I really don't want to commit to a solution that affects hundreds of lines of mathlib before making sure we never have to do that again, how about attacking a simpler end of the issue first?

The simpler end seems to be fixing the UX of search and display of such long names from the end of Doc-gen4, per my understanding, it's namely:

1. Search:

A simple idea is to break the current naming scheme into three parts: inst, SomeTypeClass and a bunch of ToXxxxxs, search should only match the first two parts, and safely ignore the third part, as they are the main source of interference to the search result.

Currently, the third part will match various parent type class, which even if it's needed by the searcher, they can still find it under "Instance for" when they found that target parent type class, no need to pollute the search result here. So it's safe to get rid of this part of match.

Implementation considerations: Doc-gen4 generates declaration data for JS to consume, this can be approached easier from the JS end to filter out this pattern.

2. Display:

Such an instance in the middle of a search result or a doc page is causing great interference to the eyes for parsing the search result or that doc page, e.g.

at this page.

A simple idea is to truncate the display exceeding a certain length, replacing it with ..., or better, just truncate it before the first To, even better, to replace the display to

closer to how they're actually written down in the source

Implementation considerations: this is likely to be implemented in Docgen4.Output but I failed to find the one rendering Instances (the one with the corresponding name is empty).

UPDATE: Some more discussion: maybe one wonders if there should be a place to have this complete name, like for copy-pasting to debug, indeed, this is a valid use case, but this use case doesn't require displaying the complete name (maybe a hint of how many characters are involved), only a "click to copy" style button can satisfy this, the complete name can safely hide in the source code of html, waiting to be copied, and staying away from human eyes.

[utensil]

Continuing:

3. There is also an issue mentioned in the Lean issue, that sometimes

the relevant link for this instance doesn't allow you to look at the equations for the instance -- you get the message One or more equations did not get rendered due to their size.

The cause of this is here which actively filters out rendered equations longer than a certain limit. This means there is no bottleneck of rendering, but the treatment of these exceedingly long rendered htmls can be improved using ideas like in the Display part mentioned above.