Topological (scoped) notation in doc-gen

Stream: general

[Filippo A. E. Nuccio]

In https://github.com/leanprover-community/mathlib4/blob/8fc0483a875e84b83c6cdb6f5c124bcbb3530370/Mathlib/Topology/Defs/Basic.lean#L189 one finds the definition of open/closed/etc... with respect to non-standard topologies, so that one can write IsOpen[T] (U : Set X), for instance, to mean that a set U is open wrt to the topology T rather than wrt any other topology that might be synthesized on X. This I find very convenient, but it does not show up in the doc-gen so that, for example, while reading docs#LinearMap.mem_span_iff_continuous_of_finite online one has no clue of the topology on E with respect to which φ would be continuous — whereas in the source this is very clear.

I wonder whether

1. is there anything that can be done to force the website to contain more notation;
2. we should embrace the policy of forcing all declarations using this notation to contain a docComment in the form/-- ... -/ (rather than just a /- ... -/ comment) so that this will show up in the website.

[Yaël Dillies]

My preference would be for n°1, by writing a custom delaborator checking for canonicity of instances. This will also be very useful in measure theory land, for the same reasons.

[Filippo A. E. Nuccio]

I completely agree, but I cannot assess how hard this would be.

[Yaël Dillies]

It should be relatively easy. Maybe open a good-first-issue on the mathlib repo?

[Thomas Murrills]

Off the top of your head, does this involve synthesizing instances during prettyprinting? If so I’ll revive my bugfix PR to core for an issue related to that. :)

[Filippo A. E. Nuccio]

I'm not entirely sure this has to do with prettyprinting, but @Yaël Dillies will certainly know better.

[Filippo A. E. Nuccio]

Yaël Dillies said:

It should be relatively easy. Maybe open a good-first-issue on the mathlib repo?

https://github.com/leanprover-community/mathlib4/issues/33238

[Yaël Dillies]

It is about pretty-printing indeed (doc-gen is a glorified pretty printer after all). There's a cheap way to write this delaborator for the most common cases (check whether there are two TopologicalSpace Foo hypotheses in context), but the proper solution would indeed involve synthesizing instances.

[Chris Henson]

Also to my knowledge, scoped notations appearing in documentation is still blocked by lean4#6050. The comments link to a previous Zulip thread. (Please upvote if like myself you find this important!)

[Aaron Liu]

linking #metaprogramming / tactics > Delaborators for `IsOpen[t]` etc here

[Eric Wieser]

Right, there is already a (open?) PR for what Yael describes

[Eric Wieser]

But if the notation is scoped it doesn't help