Documentation messed up for Submonoid.units

Stream: mathlib4

[Wrenna Robson]

I recently merged a PR adding GroupTheory/Submonoid/Units.lean. Unfortunately the documentation does not look as expected.

docs#Submonoid.units

In particular:
a) the Markdown table has not rendered as expected (despite rendering fine in separate markdown files)
b) I feel as if the "to_additives" have added a lot of extraneous proofs which, apart from anything else, make the page quite hard to read.

I want to address both of these but I don't know how. Any help?

[Wrenna Robson]

What on earth is going on with docs#AddSubmonoid.ofAddUnits_addUnits_le.match_1, for instance?

[Jireh Loreaux]

Markdown tables have different syntax depending on the parser. I can't remember which one we use, but that's my best guess without really diving in.

[Jireh Loreaux]

The to_additive seems like a doc-gen issue, @Henrik Böving ?

[Wrenna Robson]

It might be I got the configuration of to_additive wrong of course.

Reflecting in what went wrong here, btw, I realise I rarely build and look at documentation as I go, and I'm not even sure if this is part of the CI?

[Henrik Böving]

I don't have any special handling for to_additive in doc-gen.

[Wrenna Robson]

So these strange additional theorems, they must be created by to_additive itself

[Henrik Böving]

I think match_1 is just generated by the equation compiler

[Wrenna Robson]

Right. But I don't seem to have one for the originals - only the additive versions.

[Ruben Van de Velde]

I think it's more likely that they also exist for the multiplicative versions, but doc-gen successfully filters them out

[Wrenna Robson]

Aha.

[Ruben Van de Velde]

I think it's more likely that they also exist for the multiplicative versions, but doc-gen successfully filters them out

[Wrenna Robson]

So why wouldn't it filter them out for the additive versions?

[Ruben Van de Velde]

Maybe some metadata gets lost in translation? I'm not sure

[Henrik Böving]

https://github.com/leanprover/doc-gen4/blob/780bbec107cba79d18ec55ac2be3907a77f27f98/DocGen4/Process/DocInfo.lean#L120-L130 this is the logic for filtering

[Ruben Van de Velde]

I think declName.isInternal is supposed to catch those

[Eric Wieser]

Jireh Loreaux said:

Markdown tables have different syntax depending on the parser. I can't remember which one we use, but that's my best guess without really diving in.

Tables are not part of https://spec.commonmark.org/0.31.2/, and the doc-gen4 markdown parser is the reference implementation of the spec with some math hacked on, which is much less feature-rich than what we used in Lean 3

[Wrenna Robson]

Bugger

[Wrenna Robson]

So we can't do tables at all?

[Eric Wieser]

Not till we replace the markdown parser, which we already need to do anyway for non-broken math support

[Wrenna Robson]

Fair

[Wrenna Robson]

Well, it would also be good to understand why I've had this to_additive issue