!bench failing on nightly-testing

Stream: nightly-testing

[Joachim Breitner]

For example http://speed.lean-fro.org/mathlib4/run-detail/e7b27246-a3e6-496a-b552-ff4b45c7236e/3894c72cbd6f4baba45c79678e75503123a51756 has

+ temci exec --config ./scripts/bench/temci-config.yml
[2024-11-13 16:51:20,563] Program block no. 0 failed: Unexpected return code 1, expected 0
[2024-11-13 16:51:20,563] error

info: downloading component 'lean'
info: installing component 'lean'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision '42dc02bdbc5d0c2f395718462a76c3d87318f7fa'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '86d0d0584f5cd165353e2f8a30c455cd0e168ac2'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision '5ee6767b2157766c8aa451bb93d1434436e593a2'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '1383e72b40dd62a566896a6e348ffe868801b172'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '10001e92eb91fd0d186f10b8a396a98836c97f2a'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision '2adf619a966509c4e2fe129787f4b1e89601ce64'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '433429762eb5e9efb6420292b1a4be97b47cd75b'
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '726b3c9ad13acca724d4651f14afc4804a7b0e4d'
✔ [5/24] Built ProofWidgets.Compat
✔ [6/24] Built ProofWidgets.Util
✔ [7/24] Built ProofWidgets.Component.Basic
✔ [8/24] Built ProofWidgets.Cancellable
✔ [9/24] Built ProofWidgets.Component.MakeEditLink
✔ [10/24] Built ProofWidgets.Component.Panel.Basic
✔ [11/24] Built ProofWidgets.Component.Recharts
✔ [12/24] Built ProofWidgets.Component.Panel.GoalTypePanel
✔ [13/24] Built ProofWidgets.Data.Html
✔ [14/24] Built ProofWidgets.Component.FilterDetails
✔ [15/24] Built ProofWidgets.Component.HtmlDisplay
✔ [16/24] Built ProofWidgets.Component.OfRpcMethod
✔ [17/24] Built ProofWidgets.Presentation.Expr
✔ [18/24] Built ProofWidgets.Component.PenroseDiagram
✔ [19/24] Built ProofWidgets.Component.GraphDisplay
✔ [20/24] Built ProofWidgets.Data.Svg
✔ [21/24] Built ProofWidgets.Component.Panel.SelectionPanel
✔ [22/24] Built ProofWidgets.Component.InteractiveSvg
✔ [23/24] Built ProofWidgets
Build completed successfully.
error: unknown long option '--lean'

This prevents mathlib performance comparisons on lean PRs – did anyone already look in to this?

[Markus Himmel]

I think lean-pr-testing-5684 needs to be merged into nightly-testing. Cherry-picking the commit from #18354 solved it for me at #18963.

[Joachim Breitner]

Cherry-picked onto nightly-testing.