feat: add Radar setup #346
Conversation
This PR adds a Radar setup so we can track the performance of doc-gen4 builds. The benchmarks are: * `own-docs` measures the time and maxrss for building the docs for doc-gen itself. Here, it is a convenient stand-in for a moderately-sized Lean project with a moderate number of depenencies. * `mathlib-docs` measures the time and maxrss for building Mathlib's docs. We can use it to ensure that from-scratch Mathlib documentation builds don't get smaller.
|
!bench |
|
Benchmark results for 7e278bc against 5b5f81c are in! @Garmelon Runs (1🟥)
|
|
!bench |
|
Benchmark results for 7e278bc against 5b5f81c are in! @Garmelon Runs (1🟥)
|
|
Hm, it fails to get a git remote at some point in the build, and later other things fail due to heartbeat limits. |
|
!bench |
|
Benchmark results for 7361fd8 against 5b5f81c are in! @david-christiansen Runs (1🟥)
|
|
!bench |
|
Benchmark results for 24375ae against 5b5f81c are in! @david-christiansen Runs (1🟥)
|
|
!bench |
|
Benchmark results for 24375ae against 5b5f81c are in! @Garmelon No significant changes detected. |
|
!bench |
|
Benchmark results for c366b8c against 5b5f81c are in! @david-christiansen No significant changes detected. |
This better isolates the actual work of generating the docs site, and measures the correct target for Mathlib.
|
!bench |
|
Benchmark results for d560bd5 against 5b5f81c are in! @david-christiansen No significant changes detected. |
|
Seems to work, I'd merge. |
3 participants
This PR adds a Radar setup so we can track the performance of doc-gen4 builds.
The benchmarks are:
own-docsmeasures the time and maxrss for building the docs for doc-gen itself. Here, it is a convenient stand-in for a moderately-sized Lean project with a moderate number of depenencies.mathlib-docsmeasures the time and maxrss for building Mathlib's docs. We can use it to ensure that from-scratch Mathlib documentation builds don't get smaller.