readable commutative diagrams in docstrings

Stream: mathlib4

[Kevin Buzzard]

I was reviewing a PR and I found the statement of a lemma very hard to read; it said this

theorem d_eq_zero_of_f_eq_d_apply
    (x₂ : ((forget₂ C Ab).obj (S.X₂.X i))) (x₁ : ((forget₂ C Ab).obj (S.X₁.X j)))
    (hx₁ : ((forget₂ C Ab).map (S.f.f j)) x₁ = ((forget₂ C Ab).map (S.X₂.d i j)) x₂) (k : ι) :
    ((forget₂ C Ab).map (S.X₁.d j k)) x₁ = 0 := by

(and there are some variables as well). This is the kind of theorem which in my opinion would be much easier to understand with a docstring. But that docstring should contain this picture:

Screenshot from 2025-06-29 21-42-05.png

and then just say "if $x_2\in X_{2,i}$ and $x_1\in X_{1,j}$ with $f(x_1)=d(x_2)$ then $d(x_1)=0$". If I could see that picture and that one line of mathematics then not only can I immediately see what the lemma says, I can even construct a proof immediately (hint: to prove $d(x_1)=0$ it suffices to prove $f(d(x_1))=0$).

I have seen two attempts to put diagrams like this into docstrings. The first is via ASCII art. This gets garbled in the API docs. The second is via LaTeX. But the LaTeX for that commutative diagram is the incomprehensible

\[\begin{tikzcd}
    & 0 & 0 & 0 \\
    \cdots & {X_{1,i}} & {X_{1,j}} & {X_{1,k}} & \cdots \\
    \cdots & {X_{2,i}} & {X_{2,j}} & {X_{2,k}} & \cdots \\
    \cdots & {X_{3,i}} & {X_{3,j}} & {X_{3,k}} & \cdots \\
    & 0 & 0 & 0
    \arrow[from=1-2, to=2-2]
    \arrow[from=1-3, to=2-3]
    \arrow[from=1-4, to=2-4]
    \arrow[from=2-1, to=2-2]
    \arrow[from=2-2, to=2-3]
    \arrow[from=2-2, to=3-2]
    \arrow["d", from=2-3, to=2-4]
    \arrow["f", from=2-3, to=3-3]
    \arrow[from=2-4, to=2-5]
    \arrow[from=2-4, to=3-4]
    \arrow[from=3-1, to=3-2]
    \arrow["d", from=3-2, to=3-3]
    \arrow[from=3-2, to=4-2]
    \arrow[from=3-3, to=3-4]
    \arrow[from=3-3, to=4-3]
    \arrow[from=3-4, to=3-5]
    \arrow[from=3-4, to=4-4]
    \arrow[from=4-1, to=4-2]
    \arrow[from=4-2, to=4-3]
    \arrow[from=4-2, to=5-2]
    \arrow[from=4-3, to=4-4]
    \arrow[from=4-3, to=5-3]
    \arrow[from=4-4, to=4-5]
    \arrow[from=4-4, to=5-4]
\end{tikzcd}\]

so that will be unreadable in code.

What can we do here? As the abstract algebra part of mathlib grows it will get increasingly unreadable if we don't have a good solution to commutative diagrams in docstrings. Or is there already a good solution and I'm just unaware of it?

[Ruben Van de Velde]

If the ascii art gets garbled, add some backticks

[Kevin Buzzard]

ASCII art still leaves something to be desired -- the horizontal arrows are being rendered as comments and thus come out in green.

Screenshot from 2025-06-29 22-11-48.png

I still feel like ASCII art is a bit of a crappy hack. It is 2025 for goodness' sake! Credit to Gemini for doing most of the work BTW (directly from the LaTeX)

[Kevin Buzzard]

My confusion increases. Right now in Mathlib.Algebra.Homology.ShortComplex.SnakeLemma in the module docstring we have

# The snake lemma

The snake lemma is a standard tool in homological algebra. The basic situation
is when we have a diagram as follows in an abelian category `C`, with exact rows:

    L₁.X₁ ⟶ L₁.X₂ ⟶ L₁.X₃ ⟶ 0
      |       |       |
      |v₁₂.τ₁ |v₁₂.τ₂ |v₁₂.τ₃
      v       v       v
0 ⟶ L₂.X₁ ⟶ L₂.X₂ ⟶ L₂.X₃

We shall think of this diagram as the datum of a morphism `v₁₂ : L₁ ⟶ L₂` in the

which is being rendered in the API docs as

Screenshot from 2025-06-29 22-35-22.png

What made the API docs stop rendering the ASCII art midway?

[Kevin Buzzard]

Oh! Is this the old "four spaces at the start means you're writing code" thing?! Ha! Our API docs use that convention?? Is the fix "put three backticks around the ASCII art"?

[Ruben Van de Velde]

Yes, and agree that ascii art is a hack. One could imagine some kind of domain-specific language that looks like ascii art in the source but renders like tikz, but that would be Work(TM)

[Li Xuanji]

If you go down the path of doing ascii art I prefer to use unicode box-drawing characters and unicode arrows instead of - and v. They look a lot better IMO and are less likely to be misinterpreted as comments

    L₁.X₁ ⟶ L₁.X₂ ⟶ L₁.X₃ ⟶ 0
      │       │       │
      │v₁₂.τ₁ │v₁₂.τ₂ │v₁₂.τ₃
      ↓       ↓       ↓
0 ⟶ L₂.X₁ ⟶ L₂.X₂ ⟶ L₂.X₃

image.png

[Ruben Van de Velde]

Unicode art rather than ascii art, then :)

[Li Xuanji]

And here's what the original docstring might look like

       0        0         0
       │        │         │
… ───▶ X₁,i ──▶ X₁,j ─d─▶ X₁,k ──▶ …
       │        ↓ f       │
… ───▶ X₂,i ──d─▶ X₂,j ─▶ X₂,k ──▶ …
        │       │         │
… ───▶ X₃,i ───▶ X₃,j ──▶ X₃,k ──▶ …
        ↓       ↓         ↓
        0       0         0

image.png

[Kevin Buzzard]

@Li Xuanji I prefer your art solution to mine (now available here ), not least because it doesn't seem to be rendering as comments. However your f is all squashed. Can I made the vertical arrows longer somehow? What are the tricks here? Can I get a better "long down arrow" than "a bunch of U+2502's and then a \d at the end"? Should I just be cutting and pasting from the Wikipedia page? Seeing that Commodore PET keyboard and all the discussions about early Sinclair and Acorn machines reminds me of my youth :-)

[Aaron Liu]

There don't seem to be many good down arrow choices, I found ˅ (U+02C5 Modifier Letter Down Arrowhead), ↓ (U+2193 Downwards Arrow), and ꜜ (U+A71C Modifier Letter Raised Down Arrow).

[Kevin Buzzard]

If ASCII art is the state of the art and getting something much better is a nontrivial project then I'd be interested in experimenting with Unicode art

[Alex Kontorovich]

We had something similar recently in PNT+ where we wanted to draw a diagram (in a blueprint, not docstring).
image.png

[Kevin Buzzard]

I should think that Patrick would hit the roof if he saw that -- surely the point of blueprint is exactly that you can unleash Latex! But here (in theorem docstrings) we can't :-(

[Alex Kontorovich]

To get this image, I scribbled something by hand on a piece of paper, took a picture with my phone, and uploaded it to Claude, asking it to make me this image in a way that it would render in LaTeX.
image.png

[Alex Kontorovich]

Kevin Buzzard said:

I should think that Patrick would hit the roof if he saw that -- surely the point of blueprint is exactly that you can unleash Latex! But here (in theorem docstrings) we can't :-(

Ha! :) I hope he doesn't see this thread then... How would I make it in "true" LaTeX, using TikZ or something? I wasn't sure if Blueprint was set up for that...

[Kevin Buzzard]

I think I would have just made a nice picture and then included a screenshot :-) Looking at it again maybe latex isn't the right tool for that diagram!

[Kevin Buzzard]

I think blueprint is fine with tikzcd

[Alex Kontorovich]

Ok, so maybe I'll experiment with making a better picture... :)

[Kevin Buzzard]

I know it's a bit 2023 but you could try quiver and then exporting to latex and dumping it straight in blueprint

[Alex Kontorovich]

In fact, I think Claude first gave me a tikz diagram, and I was scared it wouldn't work with Blueprint, so I told it to give me text instead; so it suggested \begin{verbatim}, which blueprint accepted... So I didn't push it further...

[Kevin Buzzard]

The commutative square just after Theorem 8.7 in the FLT blueprint is done with tikzcd

[Alex Kontorovich]

Ok so I'd better change it then :joy: before Patrick sees...

[Jireh Loreaux]

Are you familiar with https://q.uiver.app/ ? We could embed links to diagrams as a general habit. Then duplicate with ASCII art. At some point, hopefully Verso could help us display these from within the editor and the ASCII art would become obsolete.

[Jireh Loreaux]

Oh I see Kevin just mentioned quiver :face_palm:

[Kevin Buzzard]

I did use it to quickly knock up the picture of the commutative diagram but it hadn't occurred to me to actually link to it!

[Robin Carlier]

Jireh Loreaux said:

Are you familiar with https://q.uiver.app/ ? We could embed links to diagrams as a general habit. Then duplicate with ASCII art. At some point, hopefully Verso could help us display these from within the editor and the ASCII art would become obsolete.

And then, whenever q.uiver is down or the service is sunset, we have useless URLs in our docs?

[Kevin Buzzard]

I mean, yes, but you could say the same thing about most of the internet (I find it frustrating that links posted on MathOverflow 15 years ago can sometimes not work...)

[Robin Carlier]

Plus the extra traffic on their server from every time someone visits lean docs.

[Robin Carlier]

Kevin Buzzard said:

I mean, yes, but you could say the same thing about most of the internet (I find it frustrating that links posted on MathOverflow 15 years ago can sometimes not work...)

Well, this applies in theory to any external url in docs (or code) that becomes an implicit dependency on an external service. E.g what happened to polarity which is now useless.

Some URLs are "less likely to go away" than others, and I wouldn't bet that quiver will be a very long term service (or just that they wouldn't make any breaking change).
I'd really prefer a self-contained solution rather than one creating a dependency.

[Robin Carlier]

(though, in the case of q.uiver, they whole thing is open source, not sure about the exact licence, so maybe if we decide to do it we should host a quiver mirror to be responsible for the traffic generated as well as making sure we don't loose every picture in our docs the day q.uiver dies)

[Ruben Van de Velde]

I mean, worst case is we have the ascii art and a broken link, best case we have ascii art and a working link

[Ruben Van de Velde]

This compared to the current situation of ascii art and no link

[Robin Carlier]

I though the suggestion was to only link (and eventually hope verso would generate pictures from links). If a ASCII/unicode art remains it's definitely better.

[Ruben Van de Velde]

Oh, that's not how I read the suggestion. If we don't keep the art, we might as well dump the unreadable tikz code into the docstring, because then you've lost the ability to see the diagram within your code editor anyway

[Kevin Buzzard]

So I think that at the very least we are saying "keep the ASCII art for now" (or perhaps "switch to unicode art but keep some kind of art") and perhaps other things are a bonus.

[Dominic Steinitz]

A solution in the Haskell ecosystem is to use the Haskell diagrams package then you have full control over your diagrams included in your documentation. I haven't looked but I don't think there is a Lean equivalent. Here's one example of a diagram I created to show how a PDE numerical scheme works as part of the documentation: https://hackage.haskell.org/package/diagrams-contrib-1.4.6/docs/Diagrams-TwoD-Grid.html.

And here's a stand alone diagram showing an atlas for the circle (not using stereographic projection - who even needs that ;-)) which I could embed in my documentation (if I so wished).

image.png

[Ruben Van de Velde]

Okay, but what does it look like in the source?

[Patrick Massot]

The blueprint should indeed have no problem with tikzcd or even tikz in general. Otherwise it’s a bug that needs a urgent fix.

[Patrick Massot]

And I agree that q.uiver.app is great. Note that it’s not more dangerous that LaTeX in term of maintenance. Hosting you own instance is trivial. You just clone the repo and serve it locally. I always have it on my laptop in case I need to work on a train or plane without internet.

[Dominic Steinitz]

Ruben Van de Velde said:

Okay, but what does it look like in the source?

The link gives the source for this image

image.png.

Do you mean for the image of the charts for the circle? I wrote that over 10 years ago. I am sure I have the source somewhere but undoubtedly it will no longer compile :-(

[Patrick Massot]

By trivial I mean

• git clone https://github.com/varkor/quiver.git
• cd quiver
• make

And then whenever you want to play locally you go to your quiver folder and type make serve which says something like Serving HTTP on 0.0.0.0 port 8000 (http://0.0.0.0:8000/) ... and then go to your webrowser and open the given url http://0.0.0.0:8000/

[Dominic Steinitz]

Ruben Van de Velde said:

Okay, but what does it look like in the source?

circleAtlas = rans <> doms <> arr1s <> arr2s <> arr3s <> arr4s
  where
    rans =    l1 # lc green  # lw 0.05
           <> l2 # lc yellow # lw 0.05
           <> l3 # lc blue   # lw 0.05
           <> l4 # lc red    # lw 0.05


    doms =        arc' 1.1 a1 a2 # lc green  # lw 0.05
           `atop` arc' 1.2 a3 a4 # lc yellow # lw 0.05
           `atop` arc' 1.1 a5 a6 # lc blue   # lw 0.05
           `atop` arc' 1.2 a7 a8 # lc red    # lw 0.05


    arr1 = arrowAt' (with & shaftStyle %~ lw 0.05 # dashing [0.05,0.05] 0.0 # lc green)
                    (p2 (0.0, 1.3))
                    ((pt1 .+^ 0.5 * (pt2 .-. pt1)) .-. (p2 (0.0, 1.3)))
    arr1s =    arr1
            <> (arr1 # translate (r2 (0.5, 0.0)))
            <> (arr1 # translate (r2 (-0.5, 0.0)))


    arr2 = arrowAt' (with & shaftStyle %~ lw 0.05 # dashing [0.05,0.05] 0.0 # lc yellow)
                    (p2 (-1.4, 0.0))
                    ((pt3 .+^ 0.5 * (pt4 .-. pt3)) .-. (p2 (-1.4, 0.0)))


    arr2s =    arr2
            <> (arr2 # translate (r2 (0.0, 0.5)))
            <> (arr2 # translate (r2 (0.0, -0.5)))


    arr3 = arrowAt' (with & shaftStyle %~ lw 0.05 # dashing [0.05,0.05] 0.0 # lc blue)
                    (p2 (0.0, -1.3))
                    ((pt5 .+^ 0.5 * (pt6 .-. pt5)) .-. (p2 (0.0, -1.3)))


    arr3s =    arr3
            <> (arr3 # translate (r2 (0.5, 0.0)))
            <> (arr3 # translate (r2 (-0.5, 0.0)))


    arr4 = arrowAt' (with & shaftStyle %~ lw 0.05 # dashing [0.05,0.05] 0.0 # lc red)
                    (p2 (1.4, 0.0))
                    ((pt7 .+^ 0.5 * (pt8 .-. pt7)) .-. (p2 (1.4, 0.0)))


    arr4s =    arr4
            <> (arr4 # translate (r2 (0.0, 0.5)))
            <> (arr4 # translate (r2 (0.0, -0.5)))


    a1 =  1 * tau / 12 :: Rad
    a2 =  5 * tau / 12 :: Rad
    a3 =  4 * tau / 12 :: Rad
    a4 =  8 * tau / 12 :: Rad
    a5 =  7 * tau / 12 :: Rad
    a6 = 11 * tau / 12 :: Rad
    a7 = 10 * tau / 12 :: Rad
    a8 =  2 * tau / 12 :: Rad


    l1 = pt1 ~~ pt2
    pt1 = p2 (1.1 * (cos $ fromRational $ toRational a1), 2.0)
    pt2 = p2 (1.1 * (cos $ fromRational $ toRational a2), 2.0)
    l2 = pt3 ~~ pt4
    pt3 = p2 (-2.0, 1.2 * (sin $ fromRational $ toRational a3))
    pt4 = p2 (-2.0, 1.2 * (sin $ fromRational $ toRational a4))
    l3 = pt5 ~~ pt6
    pt5 = p2 (1.1 * (cos $ fromRational $ toRational a5), -2.0)
    pt6 = p2 (1.1 * (cos $ fromRational $ toRational a6), -2.0)
    l4 = pt7 ~~ pt8
    pt7 = p2 (2.0, 1.2 * (sin $ fromRational $ toRational a7))
    pt8 = p2 (2.0, 1.2 * (sin $ fromRational $ toRational a8))

[Dominic Steinitz]

Just for clarity: I was suggesting writing your diagrams in Lean (declaratively) rather than using e.g. tikz. Maybe that is a bridge too far.

[Jireh Loreaux]

Patrick Massot said:

Note that it’s not more dangerous that LaTeX in term of maintenance. Hosting you own instance is trivial

Exactly, I also host my own. We could have it running on the community website easily.

[Jireh Loreaux]

Probably, we could even have a widget to parse the quiver stuff and display (or even edit) the result in the infoview, although it's beyond my expertise to implement. It would be a #quiver command that you could then call on the code.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Some thoughts:

• Infoview hovers already support MathJax, and MathJax supports AMScd. It's unfortunately a very limited package, but e.g. hovering on test below in the infoview shows a diagram

/--
$\begin{CD}
  A @>a>> B\\
  @V b V V= @VV c V\\
  C @>>d> D
\end{CD}$
-/
theorem test : True := ⟨⟩

#check id test

• Adding any visualization to hovers not in the infoview is an open problem (vscode-lean4#541).
• A PR adding support for other kinds of visualization, e.g. quiver diagram descriptions, to infoview hovers would probably be quite welcome. The community would have to come to some agreement on which format to use; quiver can parse tikz-cd code, so that might be a good solution.

[Eric Wieser]

Does the above also render in doc-gen?

[Robin Carlier]

Note that none of this works in neovim.