Zulip Chat Archive

Stream: general

Topic: Docs Markdown Table

Anatole Dedecker (Oct 07 2020 at 12:17):

I just noticed that the table is not rendered properly in the module docstring of https://leanprover-community.github.io/mathlib_docs/order/filter/interval.html Is this a recent bug, or was rendering markdown tables never a feature of the site ?

Rob Lewis (Oct 07 2020 at 12:34):

Hmm. I don't think it's new. markdown2 doesn't like this table even with the tables extra (which might need to be added to the docs). But it displays right in Bryan's observable preview.

Rob Lewis (Oct 07 2020 at 12:34):

@Bryan Gin-ge Chen any clue?

Gabriel Ebner (Oct 07 2020 at 13:13):

The mistletoe renderer that we use for the main website seems to handle the table just fine.

Eric Wieser (Oct 07 2020 at 13:17):

What renderer does mathlib_docs use?

Gabriel Ebner (Oct 07 2020 at 13:24):

markdown2

Eric Wieser (Oct 07 2020 at 13:40):

I can reproduce with

import markdown2
s = """\
| Input filter |  `Ixx = Icc`  |  `Ixx = Ico`  |  `Ixx = Ioc`  |  `Ixx = Ioo`  |
| -----------: | :-----------: | :-----------: | :-----------: | :-----------: |
|     `at_top` |    `at_top`   |    `at_top`   |    `at_top`   |    `at_top`   |
|     `at_bot` |    `at_bot`   |    `at_bot`   |    `at_bot`   |    `at_bot`   |
|     `pure a` |    `pure a`   |      `⊥`      |      `⊥`      |      `⊥`      |
|  `𝓟 (Iic a)` |  `𝓟 (Iic a)`  |  `𝓟 (Iio a)`  |  `𝓟 (Iic a)`  |  `𝓟 (Iio a)`  |
|  `𝓟 (Ici a)` |  `𝓟 (Ici a)`  |  `𝓟 (Ici a)`  |  `𝓟 (Ioi a)`  |  `𝓟 (Ioi a)`  |
|  `𝓟 (Ioi a)` |  `𝓟 (Ioi a)`  |  `𝓟 (Ioi a)`  |  `𝓟 (Ioi a)`  |  `𝓟 (Ioi a)`  |
|  `𝓟 (Iio a)` |  `𝓟 (Iio a)`  |  `𝓟 (Iio a)`  |  `𝓟 (Iio a)`  |  `𝓟 (Iio a)`  |
|        `𝓝 a` |     `𝓝 a`     |     `𝓝 a`     |     `𝓝 a`     |     `𝓝 a`     |
| `𝓝[Iic a] b` |  `𝓝[Iic a] b` |  `𝓝[Iio a] b` |  `𝓝[Iic a] b` |  `𝓝[Iio a] b` |
| `𝓝[Ici a] b` |  `𝓝[Ici a] b` |  `𝓝[Ici a] b` |  `𝓝[Ioi a] b` |  `𝓝[Ioi a] b` |
| `𝓝[Ioi a] b` |  `𝓝[Ioi a] b` |  `𝓝[Ioi a] b` |  `𝓝[Ioi a] b` |  `𝓝[Ioi a] b` |
| `𝓝[Iio a] b` |  `𝓝[Iio a] b` |  `𝓝[Iio a] b` |  `𝓝[Iio a] b` |  `𝓝[Iio a] b` |
"""
markdown2.markdown(s)

Eric Wieser (Oct 07 2020 at 13:43):

Everything works fine for me with extras=['tables'] though

Eric Wieser (Oct 07 2020 at 13:45):

https://github.com/leanprover-community/doc-gen/pull/87

Last updated: Dec 20 2023 at 11:08 UTC