doc-gen and ProofWidgets

Stream: mathlib4

[Patrick Massot]

On https://leanprover-community.github.io/mathlib4_docs/ I can read the documentation of core and Std that are used by mathlib, but no documentation of proofwidgets. Is that intentional?

[Jireh Loreaux]

Same question for Aesop?

[Henrik Böving]

If you want it you have to put it here: https://github.com/leanprover-community/mathlib4_docs/blob/main/.github/workflows/docs.yaml#L73

[Patrick Massot]

I tried to open a PR but CI doesn't seem to do anything: https://github.com/leanprover-community/mathlib4_docs/pull/2/checks. Should I simply merge this and see in production whether it works? @Henrik Böving

[Patrick Massot]

The reason I'm not sure it will work is the usual lake mess of upper case vs lower case. I have no idea what is the proper casing here, especially for ProofWidgets.

[Henrik Böving]

It uses the identifier from the lean_lib declaration in the lakefile, in the case of ProofWidgets: https://github.com/EdAyers/ProofWidgets4/blob/main/lakefile.lean#L8 so your diff should be correct. I guess we could add a test run in CI there just to be sure next time we change it though.