lean 4.7.0-rc2 breaks docs with `...`

Stream: mathlib4

[Robert Maxton]

While eliding the types of proofs and replacing elided proofs with ... makes sense in the infoview, it has also resulted in a number of opaque, uninformative docstrings. For example, docs#CategoryTheory.Over.homMk_right_down_down now reads

@[simp]
theorem CategoryTheory.Over.homMk_right_down_down {T : Type u₁} [CategoryTheory.Category.{v₁, u₁}     T] {X : T} {U : CategoryTheory.Over X} {V : CategoryTheory.Over X} (f : U.left ⟶ V.left) (w : autoParam (CategoryTheory.CategoryStruct.comp f V.hom = U.hom) _auto✝) :
⋯ = ⋯

which completely removes the thing the theorem actually proves.

It would probably be best to somehow exempt the documentation generator from such elision.

[Kyle Miller]

I'm not sure why that's a theorem -- it's stating that two proofs are equal, but that's already the case by proof irrelevance. Plus, I don't believe simp will ever rewrite proofs, so this lemma will never be used.

[Robert Maxton]

Sure, but it's just an example. There's a whole bunch of things-with-long-types that have them almost completely elided, making their docstrings mostly useless; I'm sure I could come up with a more serious example if I looked, this was just the one I happened to run across.

[Kyle Miller]

For what it's worth, the only recent difference to pp.proofs should be that it pretty prints the omitted proofs using ⋯ rather than _.

[Kyle Miller]

(@Floris van Doorn Is it expected that simps on docs#CategoryTheory.Over.homMk could generate a simp lemma on proofs?)

[Kyle Miller]

Robert Maxton said:

I'm sure I could come up with a more serious example if I looked, this was just the one I happened to run across.

If you could look for examples, that would help.

I'm not sure having proofs present inside terms is too helpful, but it would be nice if, for example, hovering over a ⋯ in the docs would show at least the type of what's being omitted.

I suppose there was one other change in a recent Lean: the option pp.proofs.withType was switched to false by default. When it's true, it would pretty print as (⋯ : p) instead. The docs could turn this option back on.

[Floris van Doorn]

Yes, simps sometimes generates equalities for propositions. See https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/simps.20generates.20useless.20lemmas/near/340927522. I just created #11622