Filter.Eventually (`∀ᶠ`) notation is not clickable in docs

Stream: mathlib4

[Aaron Hill]

In the Filter.EventuallyEq docs (under 'Equations'), the ∀ᶠ (Filter.Eventually) notation is not clickable. However, the =ᶠ[l] notation is rendered as a link, and takes you to Filter.EventuallyEq.

Is it possible to make the ∀ᶠ render as a link in the mathlib docs?

[Kyle Miller]

I had a brief go at trying to make that work about a month ago by modifying docgen, but the side effect was that parentheses in the expression would become links too.

It should be doable though in the end.

The reason that EventuallyEq works is that it's defined using notation, which causes tokens to be annotated with the head constant when the option pp.tagAppFns is true.

On the mathlib side, I suppose we could make notation3 do the same thing. It probably would work, and it wouldn't need docgen modification.

[Jireh Loreaux]

what does notation3 do for us that we can't do with notation?

[Kyle Miller]

Scoped notations and more sophisticated delaborators.

[Kyle Miller]

For example, you can't do this with notation:

notation3 "∀ᶠ "(...)" in "f", "r:(scoped p => Filter.Eventually p f) => r

[Violeta Hernández]

off-topic, but what does the 3 in notation3 stand for?

[Kyle Miller]

It has the features that Lean 3's notation command had.

[Kyle Miller]

Originally it was a compatibility command for mathport, but it's now its own thing.

I'm hoping some of the features will make it back to core eventually.

[Kyle Miller]

mathlib4#20861 has a notation3 fix for this

[Kyle Miller]

Can someone remind me if there's a way to run docgen on a branch to test this?

[Kyle Miller]

(I think I can use a similar technique in core to get dot notation to appear as links too. Edit: made lean4#6703)

[Bryan Gin-ge Chen]

We don't have anything in mathlib4 that can automatically trigger doc-gen on a branch (though maybe we should?). It'd be a bit of work, but you could maybe clone and adapt the mathlib4_docs repo, or just repeat the steps locally: https://github.com/leanprover-community/mathlib4_docs/blob/main/.github/workflows/docs.yaml

[Kyle Miller]

Thanks @Bryan Gin-ge Chen, I got building documentation locally to work with mathlib4_docs.

[Kyle Miller]

The docs are updated now. In docs#Filter.eventually_bot for example you can see links on the Eventually notation.

[Eric Wieser]

Interestingly the in and , are also highlighted

[Aaron Hill]

Thanks for fixing this!

[Eric Wieser]

It is a little weird that ∃ᶠ gets a docs link now, but not ∃!

[Kyle Miller]

@Eric Wieser It's using the rule that notation uses. It causes every token to be linked to the constant. I thought through a few different heuristics for linkifying only certain tokens, but they all fail on certain notations. Maybe in the future, if it bothers people, we could have a way to say which tokens "are" the notation for purposes of linking.

And yes, core notations will need their own treatment. I made lean4#6704 yesterday, but I might take a more drastic approach (make app unexpanders in general set the ref to the head constant, so that individual app unexpanders don't need to consider this issue).

[Jireh Loreaux]

Eric Wieser said:

Interestingly the in and , are also highlighted

This is slightly weird, but I think it's actually nice: it shows you better which bits are part of the syntax.