Fix lakeprof_report_upload

tests/bench/build/lakeprof_report_upload.py

@@ -22,7 +22,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}"
-report = run_stdout("lakeprof", "report", "-prc", cwd=src_dir)
+report = (src_dir / "lakeprof_report.txt").read_text()
 
 template = template_file.read_text()
 template = template.replace("__BASE_URL__", json.dumps(base_url))

tests/bench/build/run_bench.sh

@@ -51,6 +51,7 @@ echo ">"
 # calling lake in its current working directory.
 mv lakeprof.log "$SRC_DIR"
 pushd "$SRC_DIR"
+lakeprof report -prc > lakeprof_report.txt
 lakeprof report -pj | jq '{metric: "build/lakeprof/longest build path//wall-clock", value: .[-1][2], unit: "s"}' -c >> "$OUT"
 lakeprof report -rj | jq '{metric: "build/lakeprof/longest rebuild path//wall-clock", value: .[-1][2], unit: "s"}' -c >> "$OUT"
 popd

tests/bench/build/run_upload_lakeprof_report

@@ -1,11 +0,0 @@
-#!/usr/bin/env bash
-source ../../env_bench.sh
-
-# This should run in the same environment as run_bench, otherwise `lakeprof`
-# will use the `lake` from the global system `elan` install and not the one from
-# the current commit.
-#
-# Once an elan with support for relative toolchains has been widely released and
-# been adopted by this repo, this wrapper script should no longer be necessary
-# and the upload script can be called directly.
-./lakeprof_report_upload.py