-
Notifications
You must be signed in to change notification settings - Fork 883
Open
Conversation
@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 19, 2026
Mathlib CI status (docs):
- ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the
nightly-with-mathlibbranch. Trygit rebase bc5f89f4abe82ee105ce7922a83e286fd7a67774 --onto 58225845d6ead86550a9371cfdcb3d9f0be3fc55. You can force Mathlib CI using theforce-mathlib-cilabel. (2026年06月19日 08:52:39) - ✅ Mathlib branch lean-pr-testing-14118 has successfully built against this PR. (2026年06月22日 10:12:43) View Log
Collaborator
Reference manual CI status:
- ❗ Reference manual CI will not be attempted unless your PR branches off the
nightly-with-manualbranch. Trygit rebase bc5f89f4abe82ee105ce7922a83e286fd7a67774 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using theforce-manual-cilabel. (2026年06月19日 08:52:40) - ❗ Reference manual CI can not be attempted yet, as the
nightly-testing-2026年06月21日tag does not exist there yet. We will retry when you push more commits. If you rebase your branch ontonightly-with-manual, reference manual CI should run now. You can force reference manual CI using theforce-manual-cilabel. (2026年06月22日 09:16:51)
@hargoniX
hargoniX
force-pushed
the
hbv/grind_graph
branch
from
June 19, 2026 09:14
bd96158 to
6234f88
Compare
@hargoniX
hargoniX
changed the title
(削除) feat: cost metrics for the grind e-matching graph. (削除ここまで)
(追記) feat: cost metrics for the grind e-matching graph (追記ここまで)
Jun 19, 2026
hargoniX
commented
Jun 19, 2026
Contributor
Author
!bench
Benchmark results for 6234f88 against bc5f89f are in. No significant results found. @hargoniX
- 🟥
build//instructions: +2.2G (+0.02%)
Small changes (2✅, 2🟥)
- ✅
build/module/Lean.Meta.Tactic.Grind.Main//instructions: -353.0M (-2.61%) (reduced significance based on *//lines) - ✅
elab/big_match_partial//maxrss: -8MiB (-0.43%) - 🟥
elab/bv_decide_realworld//wall-clock: +50ms (+4.37%) - 🟥
mvcgen/sym/AddSubCancel/500/kernel//wall-clock: +7ms (+10.00%)
@hargoniX
hargoniX
force-pushed
the
hbv/grind_graph
branch
from
June 22, 2026 08:42
6234f88 to
1d8de88
Compare
@github-actions
github-actions
Bot
added
the
mathlib4-nightly-available
A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN
label
Jun 22, 2026
@mathlib-lean-pr-testing
mathlib-lean-pr-testing
Bot
added
the
builds-mathlib
CI has verified that Mathlib builds against this PR
label
Jun 22, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
This PR introduces new cost metrics for
grind's e-matching graph that can be optionally enabled in its diagnostics viaset_option grind.ematch.diagnostics true.grindis now able to detect:grind.ematch.diagnostics.branchThresholdgrindcomputes a cost metric that is roughly equivalent to the size of the transitive closure but fairly distributed among multiple parents. Configurable viagrind.ematch.diagnostics.costThreshold