Reference manual formatting

Stream: mathlib4

[David Loeffler]

I've noticed that the script that generates the mathlib HTML reference manual seems to be slightly more restrictive in the formatting it allows than the syntax highlighting in VSCode. So glitches occasionally slip through; e.g. in Mathlib.NumberTheory.Harmonic.EulerMascheroni, there's a misformatted header in the file-level docstring.

Is there a way of locally building the reference manual entry for a given file? Or, better still, is it possible to do this (and view the results) as part of CI for mathlib pull requests on github?

[Johan Commelin]

@Bryan Gin-ge Chen used to have an Observable notebook for this. But I'm not sure if it still works

[Damiano Testa]

Is the issue in this case that the header is immediately follows by a list and markdown gets confused?

[Damiano Testa]

If this is the case, this kind of issue could be mitigated by a regex.

[Damiano Testa]

Nevertheless, being able to view the rendered HTML is certainly desirable!

[David Loeffler]

Is the issue in this case that the header is immediately follows by a list and markdown gets confused?

I don't know what the issue is! That's exactly the problem – it's hard to identify what's causing formatting screwups since there's no way of testing the effect of changes. Headers immediately followed by lists are a very common idiom in the docs, so I don't know what's different about this one.

[Damiano Testa]

Indeed, Mathlib.Algebra.AddTorsor displays correctly, and seems to have similar formatting. Very weird!

[Ruben Van de Velde]

There's a non-breaking space after the ##

[Bryan Gin-ge Chen]

I haven’t updated the doc preview notebook I made for lean4 yet. I was hoping to take a look at it after doc-gen4 starts to use verso so that I can avoid having to messing around with it unnecessarily.

[David Loeffler]

There's a non-breaking space after the ##

Now that's well spotted, thank you! PR up at #12368 (I feel slightly ashamed to be submitting a PR for a single-character fix)