LaTeX in docstrings

Stream: mathlib4

[Newell Jensen]

Most docstrings in mathlib (at least from my experience) seem not to use LaTeX. What is the desired convention here? Is LaTeX something to be desired? I have no problem using LaTeX but wondering if it is something that people even want.

When reading the source code of mathlib, I would rather not have to read LaTeX source code because I have to decipher the LaTeX source in my mind while reading the docstring but when reading the generated docs I definitely prefer reading the rendered LaTeX. Thus, since I normally read the source code and not the generated docs I would tend to side with not using LaTeX.

Curious where others stand/sit on this issue?

An aside, I would love to see a way to embed rended LaTeX within the lean source files but not sure how this would even be implemented or if at all possible??

[Bryan Gin-ge Chen]

In mathlib3, if you wrote markdown with LaTeX in doc strings (embedded in the same way as you might write a question or answer on math.stackexchange or mathoverflow), doc-gen3 was able to generate HTML with the LaTeX rendered by MathJax.

In principle we could with some effort port the same collection of hacks over to doc-gen4, but my impression is it's probably better to wait until Verso is ready for this sort of thing.

[Newell Jensen]

Looks like LaTeX in docstrings is still working for mathlib4 from what I can see here for example

But maybe you are referring to something else?

[Bryan Gin-ge Chen]

(Ah, I guess doc-gen4 has some LaTeX + markdown capabilities, but compare your example to the output of doc-gen3.)

Reading over your first message in the thread again, I think I missed the point the first time around. Sorry for the noise!

[Newell Jensen]

Yeah, there are some differences there between the outputs. No worries! Better than silence ;P

[Eric Wieser]

A good compromise is sometimes to use latex with unicode math

[Oliver Nash]

I only resort to LaTex after convincing myself that pure unicode just can't do the job. This usually happens only in longer text, such as module doc strings.

[Eric Wieser]

A rule I'd propose is to use unicode (in backticks) if it's (almost) valid lean syntax, otherwise use latex (preferring unicode math where possible). Using pseudo code that's neither correct lean nor pretty LaTeX seems like a bad compromise to me

[Eric Wieser]

Often a good use of LaTeX in a docstring is when the lean statement is becoming hard to read, since someone reading the web docs can most likely read the "regular math" faster than the lean statement