mermaid diagrams in docgen

Stream: mathlib4

[Jireh Loreaux]

If I put a mermaid diagram in a library note, will docgen render it? I thought it would, but I was having trouble building the documentation locally in order to find out.

[Jireh Loreaux]

Context: #22172

[Eric Wieser]

I strongly suspect the answer is no, but we could probably make a PR to doc-gen after the fact

[Jz Pan]

As far as I know, no. In order to implement it I think we need to postprocess the HTML returned by md4c, filter the <code class="language-mermaid"> and send the contents of it to external program.

And now we can't insert pictures in doc-gen yet. This need to be developed as we need a way to track external pictures which probably will be generated by the above external program.

By the way, I think currently doc-gen does not render library note at all?

[Eric Wieser]

I think mermaid runs client side?

[Eric Wieser]

So all we have to do is add the JavaScript to the page template

[Jireh Loreaux]

But we still need doc-gen to load the script

[Jz Pan]

Jireh Loreaux said:

But we still need doc-gen to load the script

Then it's easy, just modify the template file is OK.

[Jz Pan]

https://github.com/leanprover/doc-gen4/blob/main/DocGen4/Output/Template.lean

[Jireh Loreaux]

As Jz Pan points out, we don't currently do anything with library notes in docgen, so this is moot. (See: https://leanprover-community.github.io/mathlib4_docs/Mathlib/Algebra/HierarchyDesign.html)

[Jireh Loreaux]

@Frédéric Dupuis what would you like me to do for #22172? Make an ASCII art diagram?

[Eric Wieser]

I think we should merge as is with mermaid, and then make a PR to doc-gen

[Eric Wieser]

The mermaid isn't going to be rendered in VSCode anyway, but it's easy enough to render online via https://codapi.org/mermaid/ for someone who wants to look at it while we work out what doc-gen should do

[Jz Pan]

Is library_note a feature for core Lean or only for mathlib? If it's latter, I've remembered that doc-gen will not add features only work for mathlib...

Technical level, I think it's not hard to rendere library_note, just pretend it to be a /-! ... -/, adds a header ## Library note: <name> then append the contents of /-- ... -/.

[Frédéric Dupuis]

Jireh Loreaux said:

Frédéric Dupuis what would you like me to do for #22172? Make an ASCII art diagram?

I think I would vote for ASCII art, it's not a very big diagram, and my guess is that people won't bother to figure out how to compile it.

[Jireh Loreaux]

So, ASCII art in a code block? That way, when it does get rendered elsewhere, the ASCII art isn't destroyed by a kerned font?

[Frédéric Dupuis]

Yeah

[Riccardo Brasca]

Maybe chatgpt can do it for you

[Jireh Loreaux]

mermaid-ascii exists

[Eric Wieser]

It seems to me like the ~5 line change to doc-gen is easier than any of these options

[Jz Pan]

Eric Wieser said:

It seems to me like the ~5 line change to doc-gen is easier than any of these options

The problem is that it does not render in VSCode pop-up tooltips.

[Jireh Loreaux]

@Frédéric Dupuis I've switched to ASCII-art in #22172

[Eric Wieser]

The problem is that it does not render in VSCode pop-up tooltips.

This doesn't happen in library notes anyway