CI preview of compiled docs

Stream: mathlib4

[David Loeffler]

I saw Kevin's announcement about BdR, and went to browse the docs to see more about what has been added. In the process, I noticed that the docstrings for the new declarations are full of formatting glitches.

Screenshot 2025-12-01 at 08.07.30.png

This kind of glitch is very common unfortunately, because if you use any kind of formatting in docstrings, you're essentially "flying blind": there's no way to check if the markup you've used is actually correct, since the reference manual doesn't get built until after the PR is merged. (I guess you can preview docstrings for individual declarations using mouse hover, but not file-level docstrings.)

Is there any way we can make it possible for the CI build step to also build a copy of the docs that authors and reviewers can inspect, so this kind of documentation mistake can be caught before merging?

[Yaël Dillies]

In fact, @Bryan Gin-ge Chen has an Observable template to do exactly this kind of inspection. It is little known, unfortunately

[David Loeffler]

One of the more common LaTeX errors seems to be either $$ ... $$ or \( ... \) used for inline math (where the doc gen engine expects $ ... $). Is there any way of teaching the doc generation script to understand \( ... \)?

[David Loeffler]

(And I suppose there is no hope of teaching the mouse-over hover in VS Code to compile latex in docstrings on-the-fly?)

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

There is hope, though I don't know if anyone is working on it; vscode-lean4#541.

[David Loeffler]

Interesting, I had always assumed the infoview and editor tooltips were implemented the same way, I hadn't realised one had this feature already.

[David Loeffler]

I made this PR to fix numerous instances of misformatted inline latex, excluding the BdR file since Riccardo has already asked @Jiang Jiedong to fix that.

[David Loeffler]

oops, forgot the PR link: #32299

[David Loeffler]

@Yaël Dillies , @Bryan Gin-ge Chen I'd be grateful if you could tell me how I can try out this observable template on that PR.

[Yaël Dillies]

Here's Bryan's Observable notebook. For future reference, searching on Zulip for "observable¨ + sent by Bryan finds it.

[Kevin Buzzard]

Yeah but that requires remembering "observable" rather than what I actually remember, which is "that cool thing that Bryan did years ago for viewing docstrings" (and which I had assumed stopped working when we switched to mathlib4 like many other such tools did -- apparently not!).

There are a ton of "hidden gems" in this Zulip, for example Bryan's work cited above, the triage dashboard, the mathlib changelog, new semantic search engines such as Leandex and so on. These are just things useful to me -- other people will have their own lists. I've just taken to having a "useful Lean links" bookmark directory which I now sync between machines (and to which I've now added Bryan's notebook) but I wonder if we can do better somehow.

[Yaël Dillies]

cc @Anne Baanen, maybe Bryan's notebook should be on the resources page

[Jiang Jiedong]

Oh thanks! I'll fix the display problem at once. I didn't realize that \( \) does not work in docs page. Only $ ... $ works.