chore: get lakeprof upload url from env var (#14355)

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.

Author: Garmelon

tests/bench/build/README.md

@@ -38,5 +38,5 @@ The following metrics are collected individually for each module:
 - `build/module/<name>//bytes .olean.server`
 - `build/module/<name>//bytes .olean.private`
 
-If the file `build_upload_lakeprof_report` is present in the repo root,
-the lakeprof report will be uploaded once the benchmark run concludes.
+If the `LAKEPROF_UPLOAD_URL` environment variable is set,
+the lakeprof report will be uploaded to that URL prefix once the benchmark run concludes.

tests/bench/build/lakeprof_report_upload.py

@@ -1,10 +1,17 @@
 #!/usr/bin/env python3
 
 import json
+import os
 import subprocess
 import sys
 from pathlib import Path
 
+upload_url = os.environ.get("LAKEPROF_UPLOAD_URL")
+if not upload_url:
+    sys.exit(0)
+if upload_url.endswith("/"):
+    upload_url = upload_url[:-1]
+
 # Determine paths relative to the current file.
 script_file = Path(__file__)
 template_file = script_file.parent / "lakeprof_report_template.html"
@@ -21,7 +28,7 @@ def run_stdout(*command: str, cwd: Path | None = None) -> str:
 
 
 sha = run_stdout("git", "rev-parse", "@", cwd=src_dir).strip()
-base_url = f"https://speed.lean-lang.org/lean4-out/{sha}"
+base_url = f"{upload_url}/{sha}"
 report = (src_dir / "lakeprof_report.txt").read_text()
 
 template = template_file.read_text()