Skip to content

Conversation

@Kha
Copy link
Member

@Kha Kha commented Jun 11, 2025

Corresponding to Kha/lean-bench@d3f39f8

@Kha
Copy link
Member Author

Kha commented Jun 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit 7bef7f0.
The entire run failed.
Found no significant differences.

@github-actions github-actions bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Jun 11, 2025
@leanprover-community-bot
Copy link
Collaborator

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cf8315ed962b989f7d3b5da0a0d85fef49c460ac --onto 0a9c24649767dea857a388e5385b7ae94bfd0185. You can force Mathlib CI using the force-mathlib-ci label. (2025-06-11 08:58:37)

@Kha Kha force-pushed the push-mnwrpkulkqlm branch from 7bef7f0 to f0ff2a8 Compare June 11, 2025 09:17
@Kha
Copy link
Member Author

Kha commented Jun 11, 2025

!bench

@leanprover-bot
Copy link
Collaborator

Here are the benchmark results for commit f0ff2a8.
There were significant changes against commit cf8315e:

  Benchmark        Metric       Change
  ===============================================
+ rbmap_10         task-clock    -1.0%  (-21.0 σ)
+ rbmap_10         wall-clock    -1.0%  (-20.3 σ)
- riscv-ast.lean   wall-clock     6.0%   (95.4 σ)
+ stdlib           blocked       -1.8%  (-46.7 σ)
+ stdlib           grind simp    -1.1% (-180.5 σ)

@Kha Kha added this pull request to the merge queue Jun 11, 2025
Merged via the queue into leanprover:master with commit 01a0524 Jun 11, 2025
15 checks passed
@Kha Kha deleted the push-mnwrpkulkqlm branch June 12, 2025 16:13
algebraic-dev pushed a commit to algebraic-dev/lean4 that referenced this pull request Jun 18, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants