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

[Moritz Doll]

Heyhey, I am sorry to resurrect an old thread, but I just noticed that https://leanprover-community.github.io/mathlib4_docs/Mathlib/Analysis/Distribution/SchwartzSpace.html#Schwartz-space had its LaTeX replaced by backticks. My personal rule was similar to what Eric wrote above and so I am slightly confused because the change IMO contradicts that. I have no particularly strong opinions on the matter, but is it the consensus now that we only use LaTeX only if backticks are almost impossible?

[Eric Wieser]

I guess that was #32299

[Eric Wieser]

(cc @Johan Commelin who merged it and @David Loeffler who PR'd it)

[David Loeffler]

I wasn't aware of this previous debate, sorry. In the file in question, I thought "... all multiindices $α, β$" definitely didn't need to be latexed, but with the other formula I agree it's less clear-cut and I probably should have left it be. If @Moritz Doll wants it changed back I certainly have no objection.

[Johan Commelin]

Same for me

[Martin Dvořák]

I am a big fan of Unicode and avoid LaTeX when possible.

My opinion could be heavily biased by the fact that I read the code much more often than the autogenerated docs. One of the reason (but definitely not the only reason) is that searching in the docs gives me "Cannot fetch data, please check your network connection. TypeError: Failed to fetch" almost every time, and so, when I want to look up something in the docs, I usually go to Zulip and send a message to myself with docs hashtag keyword, which works almost always; however, as this process is time-consuming, I almost always end up searching in the code directly.

[Snir Broshi]

Martin Dvořák said:

I usually go to Zulip and send a message to myself with docs hashtag keyword, which works almost always; however, as this process is time-consuming, I almost always end up searching in the code directly.

You can skip Zulip if you use the same template it uses for docs URLs:
https://leanprover-community.github.io/mathlib4_docs/find/?pattern=your-query-here#doc
I think it's even possible to add this as a "search engine" in most browsers, which should let you type e.g. "docs" then press tab, write the query and press enter

[Eric Wieser]

I usually use loogle as a faster docs search

[Moritz Doll]

David Loeffler said:

I wasn't aware of this previous debate, sorry. In the file in question, I thought "... all multiindices $α, β$" definitely didn't need to be latexed, but with the other formula I agree it's less clear-cut and I probably should have left it be. If Moritz Doll wants it changed back I certainly have no objection.

No worries! I am less interested in what to do in this particular file (I liked how it was, but that is a very personal preference), but more what the guiding principles are. I was using LaTeX there because the definition with multiindices is not at all what we do in mathlib, so I was thinking that writing α, β instead of $\alpha, \beta$ is misleading because it implies the definition is using multiindices.
There is a closely related question, namely where LaTeX is appropriate. I wouldn't want to use it in doc-strings for definitions or theorems, but only in module docstrings, basically the module docstring says what maths concept is being formalized and can refer to the formal and informal world, whereas the theorems and definitions only refer to the formalized world.
But as I said this is purely my own way of doing things and I think it would be nice to talk about this and I am interested in other opinions.

[David Loeffler]

Personally I'm a strong believer in "use unicode math if at all possible" (only switching to LaTeX if the unicode version is completely illegible). My reason for this is that swapping between dialects involves a certain amount of friction – particularly with things like calligraphic alphabets, where understanding the text might crucially require you to work out that $\mathcal{A}$ and 𝒜 are supposed to be the same as each other, but both are different from $\mathscr{A}$. So I prefer to keep this code-switching to a minimum – and since a very large chunk of the mathematical text in mathlib is absolutely required to be in unicode, that means playing along with that in docstrings etc as well. But clearly there is room for multiple views on this; we can adopt the rule "contributor decides for their own contributions" (as we do for American / British English in spelling, etc).

[David Loeffler]

(@Moritz Doll I'm curious whether your thumbs-up is pointing to the last sentence of my post, the rest of it, or both :-) )

[Moritz Doll]

Haha, mainly as a I can see you point (even though I disagree on the conclusion). I think that switching a lot is not good, but I don't think that that implies not to use LaTeX at all. In the file that started the discussion, the module docstring was fully in LaTeX (if I remember correctly) and the contents there were somewhat far from the actual formalization.
I also agree that having some contributer's choice is good.
Finally, I respect opinions I disagree with (:thumbs_down: feels borderline passive-aggressive to me, when used for anything other than "you are factually wrong") :smile:

[David Loeffler]

Here is a PR to revert the change: #32890

[Michael Rothgang]

I like a tradition of "instead of :-1:-ing a post, write one explaining why you disagree (which can be in friendly words!) - and then other can :+1: that one. Very often, that works very well.

[Michael Rothgang]

The rust project disabled the :-1: reaction on github for this reason.

[Eric Wieser]

Michael Rothgang said:

The rust project disabled the :-1: reaction on github for this reason.

I thought you couldn't configure the standard 8 reactions

[Michael Rothgang]

It might be that github has disabled :-1: themselves now. (Rust did this a number of years ago; maybe that was different then.)