doc-gen links to modules

Stream: general

[Kevin Buzzard]

I am a bit bewildered by the following. In the module docstring for Mathlib.AlgebraicGeometry.EllipticCurve.Jacobian there is a mention of Mathlib.AlgebraicGeometry.EllipticCurve.Group here and 17 lines later in the same module docstring there's a mention of Mathlib.AlgebraicGeometry.EllipticCurve.Affine here. But in the docs the first of these links is broken (it links to the definition of a group) whereas the second one works fine. Is this a bug?

[Ruben Van de Velde]

Annoyingly, docgen only creates links to modules that are imported in the current file

[Eric Wieser]

Does that also apply to Mathlib/Foo/Bar.lean-style references?

[Ruben Van de Velde]

No (because those don't check the target file exists at all)

[Ruben Van de Velde]

I'm holding out on replacing them all in case verso does something smarter

[Kevin Buzzard]

The un-xy here is that #20037 (amongst other things) makes the change to Mathlib/AlgebraicGeometry/EllipticCurve/Group.lean in this file (and I was asking precisely because I was trying to review the PR and was wondering what the heck was going on here)

[Eric Wieser]

I think we should replace all the file links with .lean, even if verso will eventually do something cleverer; because at the end of the day we need separate syntax for linking imports and linking declarations, as they can occupy the same names.

[Eric Wieser]

The verso cleverness would probably be :file:`Mathlib.Vector` vs :decl:`Mathlib.Vector` or similar, which is a much easier grep if we have the .lean suffixes to distinguish them

[Ruben Van de Velde]

You convinced me enough to still do nothing but also not complain if someone else does it :)