chore: get lakeprof upload url from env var

[Garmelon]

This PR allows the bench repo to decide whether and where to upload the lakeprof report. This brings this bench suite more in-line with the others like mathlib's or cslib's.

[Garmelon]

!bench

[leanprover-radar]

Benchmark results for d6c2533 against 8006bb0 are in. There are significant results. @Garmelon

Warning

These warnings may indicate that the benchmark results are not directly comparable, for example due to changes in the runner configuration or hardware.

• Bench repo commit hashes for run build differ between commits.
• Bench repo commit hashes for run other differ between commits.

• 🟥 build//instructions: +271.6M (+0.00%)

New metrics (2✅, 3🟥)

• 🟥 elab/verina//cycles: +72.2M (+0.12%)
• ✅ elab/verina//instructions: -18.0M (-0.02%)
• 🟥 elab/verina//maxrss: +14MiB (+1.77%)
• ✅ elab/verina//task-clock: -2ms (-0.02%)
• 🟥 elab/verina//wall-clock: +7ms (+0.26%)

Large changes (1🟥)

• 🟥 build/profile/interpretation//wall-clock: +1s (+1.70%)

Small changes (4🟥)

• 🟥 lake/inundation/config import//maxrss: +4MiB (+0.43%)
• 🟥 lake/inundation/config tree//maxrss: +3MiB (+0.39%)
• 🟥 lake/inundation/env//maxrss: +4MiB (+0.44%)
• 🟥 lake/inundation/startup//maxrss: +3MiB (+2.58%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-07-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-10 16:17:08)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase dd8e885bf12ec43c87046fd1484e29384d04ea6c --onto da19ea085d7cdba0131ec59b4f678b0910304878. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-10 16:40:47)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 501e4e81986cf04b38987d8f2647da8a0e099760 --onto 12c859a4d735fbcdb3ebbddb42dcc8619bcc7a7d. You can force Mathlib CI using the force-mathlib-ci label. (2026-07-14 12:49:02)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-07-10 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-07-10 16:17:10)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase dd8e885bf12ec43c87046fd1484e29384d04ea6c --onto da19ea085d7cdba0131ec59b4f678b0910304878. You can force reference manual CI using the force-manual-ci label. (2026-07-10 16:40:48)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 501e4e81986cf04b38987d8f2647da8a0e099760 --onto 7847ce51363794755252279e6732240bd4f27ca8. You can force reference manual CI using the force-manual-ci label. (2026-07-14 12:49:04)

[MohammedAlkindi]

This looks like a good opt-in/configurability change. One coordination question before approval:

tests/bench_build.sh still calls tests/bench/build/lakeprof_report_upload.py unconditionally at the end of the radar build benchmarking flow. Since this script previously uploaded to https://speed.lean-lang.org/lean4-out/{sha} by default, merging this PR will make production lakeprof uploads silently stop unless radar's CI/config is updated to set, for example:

LAKEPROF_UPLOAD_URL=https://speed.lean-lang.org/lean4-out

Has that matching radar change already been made or planned alongside this PR?

[Garmelon]

!bench

[leanprover-radar]

Benchmark results for 65ad36b against 501e4e8 are in. There are significant results. @Garmelon

• 🟥 build//instructions: +543.2M (+0.00%)
• 🟥 build exited with code 1

Small changes (2✅, 1🟥)

• 🟥 compiled/watchdogRss//instructions: +61.7M (+0.24%)
• ✅ lake/inundation/config import//maxrss: -4MiB (-0.45%)
• ✅ lake/inundation/env//maxrss: -4MiB (-0.44%)

[Garmelon]

!bench

[leanprover-radar]

Benchmark results for b14fda5 against 501e4e8 are in. No significant results found. @Garmelon

• 🟥 build//instructions: +1.5G (+0.01%)

Medium changes (1✅)

• ✅ lake/inundation/startup//maxrss: -6MiB (-5.43%)

Small changes (3✅, 1🟥)

• 🟥 compiled/watchdogRss//instructions: +62.2M (+0.24%)
• ✅ lake/inundation/config import//maxrss: -6MiB (-0.67%)
• ✅ lake/inundation/config tree//maxrss: -5MiB (-0.62%)
• ✅ lake/inundation/env//maxrss: -6MiB (-0.65%)