Problems building HTML documentation

Stream: mathlib4

[Stefan Kebekus]

Dear all,

I would like to improve the Mathlib4 documentation a bit, but I am running into trouble. According to https://github.com/leanprover-community/mathlib4 I can build HTML documentation (and thereby see my changes) using

lake -Kdoc=on build Mathlib:docs

but that does not work:

error: unknown library facet `docs`

I would be grateful for any hint or advice.

Best,

Stefan.

[Damiano Testa]

The html documentation files are autogenerated from the Mathlib source code. So, usually, improving the documentation means modifying the doc-strings. Is this what you are trying to do?

[Damiano Testa]

In particular, you should not need to build the docs locally, but directly edit the .lean files and then a bot refreshes the documentation on a schedule.

[Kim Morrison]

On this subject, the README is wrong about updating dependencies in Mathlib. It currently says:

If you are a mathlib contributor and want to update dependencies, use lake update -Kdoc=on. This will update the lake-manifest.json file correctly. You will need to make a PR after committing the changes to this file.

But one should not include -Kdoc=on here, because we do not keep the doc-gen dependencies in our lake-manifest.json, because only automatic processes should ever be running doc-gen!

[Kim Morrison]

#14109

[Kim Morrison]

@Stefan Kebekus, I agree with @Damiano Testa's response that probably you should not be running doc-gen yourself: it's unnecessary and better left to automation, unless you are changing specific things about the layout or behaviour of the documentation pages, rather than just the content.

[Ruben Van de Velde]

I think it would be helpful if there was an easy way to check that your documentation changes render as expected, though

[Kim Morrison]

That said, I'm guessing the instructions are mean to actually be:

lake -R -Kdoc=on update doc-gen4
lake build Mathlib:docs

(but then make sure not to commit your lake-manifest.json in your next commit!)

[Stefan Kebekus]

@Damiano Testa @Kim Morrison Thank you, as always, for the quick and helpful replies.

I understand from your answers that GitHub will build the documentation automatically. Still, I feel that the issue should be addressed:

• There are settings [experimenting with Markdown tables] where iterations via GitHub could be lengthy and painful.
• Unless I made a mistake running lake [which is totally possible], I feel that the documentation in README.md should be correct or else be deleted. Perhaps we could replace the current text with a warning 'Do not try to build HTML docs yourself' and a 'Here's how to do that in GitHub'?

What do you think? Does that make sense?

[Kim Morrison]

Our messages passed each other. :-) I'm just running those commands now, and once I see how long they take to run I will update the README.

[Stefan Kebekus]

I have to run away now, but should be back in the evening.

[Kim Morrison]

Unfortunately it will still be pretty lengthy and painful running locally. Building the docs is a nontrivial task, from what I understand greater than just building mathlib from scratch, so >20minutes even on a big machine.

[Yaël Dillies]

Ruben Van de Velde said:

I think it would be helpful if there was an easy way to check that your documentation changes render as expected, though

Bryan's Observable notebook is a thing, but for Lean 3 currently. It should still be mostly accurate

[Henrik Böving]

Kim Morrison said:

Unfortunately it will still be pretty lengthy and painful running locally. Building the docs is a nontrivial task, from what I understand greater than just building mathlib from scratch, so >20minutes even on a big machine.

Mathlib takes less than 20 minutes to compile on a big machine? The current run times for doc-gen in its CI are round about 12 min

[Henrik Böving]

Oh and of course note that thanks to lake doc-gen gets incremental builds for free so I would at least hope that rebuilds that only change individual files are fast.

[Kim Morrison]

lake build Mathlib:docs  21147.62s user 4743.04s system 1901% cpu 22:41.92 total

[Kim Morrison]

Sad, maybe Apple Silicon and doc-gen don't like each other.

[Henrik Böving]

I based my time on this one https://github.com/leanprover-community/mathlib4_docs/actions/runs/9654318504/job/26628315358, maybe that machine is just fancier than yours :shrug:

[Kim Morrison]

Note that the lake -R -Kdoc=on update doc-gen4 command required to setup doc-gen4 locally means that you can't use a cache from CI and have to do a local build.

[Kim Morrison]

Somehow that is not happening in the CI run you linked to, however...?

[Henrik Böving]

Ah yes, the CI cleverly cheats around that by creating a project that requires mathlib instead of playing with the conditional dependencies in mathlib's lakefile.

[Kim Morrison]

#14114 fixes the README

[Stefan Kebekus]

@Kim Morrison Thank you for fixing this. With your help, I could generate the documentation and submit my first documentation-improving PR today.

[Stefan Kebekus]

@Yaël Dillies Bryan's Observable notebook did indeed work well for me. Thank you for the link.

[Bryan Gin-ge Chen]

Stefan Kebekus said:

Yaël Dillies Bryan's Observable notebook did indeed work well for me. Thank you for the link.

Glad to hear the notebook is still useful!

Be advised that there may be differences between how doc-gen4 processes LaTeX in markdown and how the notebook works. When development of doc-gen4 has stabilized, I'm planning to create a lean4 version of the notebook at some point but until then make sure to double-check the generated output (especially for LaTeX) on the mathlib4_docs page or a local build.

Feel free to ping me if you notice any discrepancies, of course.