Zulip Chat Archive

Stream: general

Topic: Can't click on some mathlib3 docs

Kevin Buzzard (Jun 16 2023 at 07:41):

The web page https://leanprover-community.github.io/mathlib_docs/field_theory/galois.html won't let me click on fixed_field. Is this expected?

Screenshot-from-2023-06-16-08-40-50.png

Yaël Dillies (Jun 16 2023 at 07:42):

docs#fixed_field doesn't exist. Do you mean docs#intermediate_field.fixed_field ?

Kevin Buzzard (Jun 16 2023 at 07:42):

I just mean "something isn't working and I'm not sure what". Mathematically yes, the claims are about the declaration you suggest.

Mario Carneiro (Jun 16 2023 at 07:43):

I think it's because of the namespace? How does autolinking in mathlib3 work anyway?

Yaël Dillies (Jun 16 2023 at 07:44):

Whoever wrote that docstring is referring to a declaration that doesn't exist. I don't know what that declaration is, but if it intermediate_field.fixed_field then you should simply replace fixed_field by intermediate_field.fixed_field.

Kevin Buzzard (Jun 16 2023 at 07:45):

Got it. So this has been the case throughout the docs? That fully qualified names are needed? I'm somehow surprised that the docs are even readable if this is the case.

Yaël Dillies (Jun 16 2023 at 07:45):

Yes, you need to fully qualify names everywhere.

Mario Carneiro (Jun 16 2023 at 07:45):

From what I can tell by poking around only fully qualified names are autolinked

Mario Carneiro (Jun 16 2023 at 07:45):

TBH I'm in agreement with Kevin that this is terrible

Mario Carneiro (Jun 16 2023 at 07:46):

and fully qualifying everything is not a solution, it would make things even worse

Mario Carneiro (Jun 16 2023 at 07:48):

I mean, this was never particularly readable: image.png

Mario Carneiro (Jun 16 2023 at 07:48):

when I see this kind of thing in the docs I just go to the source

Kevin Buzzard (Jun 16 2023 at 07:56):

So does docs#fixing_subgroup exist? Huh, it does. So there is some asymmetry in namespace conventions here. In mathlib4 this declaration is also namespaced!

Eric Wieser (Jun 16 2023 at 22:33):

Mario Carneiro said:

TBH I'm in agreement with Kevin that this is terrible

The alternative of taking into account open namespaces doesn't work because we don't allow opening namespaces before module docstrings

Scott Morrison (Jun 17 2023 at 00:15):

haha, we could open namespaces via time travel for the purposes of hyperlinking. (i.e. scan the whole file for open statements, and use future ones if you can't already resolve the name)

Mario Carneiro (Jun 17 2023 at 00:22):

...or just allow module docs do go anywhere?

Last updated: Dec 20 2023 at 11:08 UTC