Zulip Chat Archive

Stream: mathlib4

Topic: autolinking files in docs

Yury G. Kudryashov (May 28 2023 at 22:55):

Hi, does mathlib4 api doc builder autolinks files? If yes, then which syntax? Mathlib.Algebra.Group.Basic, Algebra.Group.Basic, or Algebra/Group/Basic?

James Gallicchio (Jun 01 2023 at 00:13):

@Henrik Böving would know

Eric Wieser (Jun 01 2023 at 00:45):

I think we should consider adding a custom syntax for this to ensure that we actually refer to files that exist

Eric Wieser (Jun 01 2023 at 00:45):

https://myst-tools.org/ does something like this

James Gallicchio (Jun 01 2023 at 01:19):

Yeah, and resolving them in the same way that lake resolves imports seems reasonable. I think there's already an API in lake for doing so.

Henrik Böving (Jun 01 2023 at 06:13):

Yury G. Kudryashov said:

Hi, does mathlib4 api doc builder autolinks files? If yes, then which syntax? Mathlib.Algebra.Group.Basic, Algebra.Group.Basic, or Algebra/Group/Basic?

If you mean within doc strings then no

Ruben Van de Velde (Jun 01 2023 at 07:15):

Henrik Böving said:

Yury G. Kudryashov said:

Hi, does mathlib4 api doc builder autolinks files? If yes, then which syntax? Mathlib.Algebra.Group.Basic, Algebra.Group.Basic, or Algebra/Group/Basic?

If you mean within doc strings then no

Can "we" make it so? :)

Henrik Böving (Jun 01 2023 at 07:54):

In theory sure, it would be generally cool if we could agree on some form of markdown based documentation format because right now all of the linking in the docs is on a purely heuristical basis

Last updated: Dec 20 2023 at 11:08 UTC