mathlib4_docs build times doubled?

Stream: mathlib4

[Bryan Gin-ge Chen]

buildtimes.png

I was looking over mathlib4_docs workflow runs and noticed that after Jan 3 the build times went from <20m to >45m. Is this expected?

Looking over recent doc-gen4 commits, it seems that the only changes in the relevant time period are a bump to v4.16.0-rc1 and switching to a fork of md4lean.

[Michael Rothgang]

Looking at a previous and current build log, the step taking much longer is indeed the "generate docs" step.

[Michael Rothgang]

Looking at the commit log, I wonder about https://github.com/leanprover/doc-gen4/commit/4d618d6b49d145f67ae63b56238adec41b7e53b4 (i.e. adapting doc-gen for lean4#6388 --- the diff is a significant change.

@Mac Malone Do you have an idea if this change could have caused doc-gen4 to slow down by a factor of 3 or 4?

[Henrik Böving]

No

[Henrik Böving]

You need to read the log more carefully

✔ [753/12035] Built Mathlib.Init
✔ [754/12035] Built Mathlib.Init:docs
✔ [755/12035] Built Mathlib.Data.Int.Notation
✔ [756/12035] Built Mathlib.Data.Int.Notation:docs
✔ [757/12035] Built Mathlib.Data.Nat.BinaryRec
✔ [758/12035] Built Mathlib.Data.Nat.BinaryRec:docs
✔ [759/12035] Built Mathlib.Data.Nat.Notation
✔ [760/12035] Built Mathlib.Data.Nat.Notation:docs
✔ [761/12035] Built Mathlib.Data.String.Defs
✔ [762/12035] Built Mathlib.Data.String.Defs:docs
✔ [763/12035] Built Mathlib.Data.Array.Defs
✔ [764/12035] Built Mathlib.Data.Array.Defs:docs
✔ [765/12035] Built Mathlib.Util.MemoFix
✔ [766/12035] Built Mathlib.Util.MemoFix:docs
✔ [767/12035] Built Mathlib.Lean.Expr.ReplaceRec
✔ [768/12035] Built Mathlib.Lean.Expr.ReplaceRec:docs
✔ [769/12035] Built Mathlib.Lean.EnvExtension
✔ [770/12035] Built Mathlib.Lean.EnvExtension:docs
✔ [771/12035] Built Mathlib.Lean.Meta.Simp
✔ [772/12035] Built Mathlib.Lean.Meta.Simp:docs

As you can see here it is building both mathlib and the documentation, the issue is that the mathlib cache is broken with the 4.16.0-rc1 so it has to rebuild that as well, the extra time here is just compiling mathlib, doc-gen is as fast as ever

[Bryan Gin-ge Chen]

Aha, I think that explains it then. Thanks!