Skip to content

restrict lazy WHNF to reducible (test)#13702

Draft
datokrat wants to merge 2 commits into
masterfrom
paul/test/disable-lazywhnfcore
Draft

restrict lazy WHNF to reducible (test)#13702
datokrat wants to merge 2 commits into
masterfrom
paul/test/disable-lazywhnfcore

Conversation

@datokrat
Copy link
Copy Markdown
Contributor

@datokrat datokrat commented May 11, 2026

No description provided.

@datokrat
Copy link
Copy Markdown
Contributor Author

datokrat commented May 11, 2026

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented May 11, 2026 •
edited
Loading

Benchmark results for d6ea09d against a71f158 are in. There are significant results. @datokrat

  • ✅ build//instructions: -18.8G (-0.16%)

Large changes (1✅)

  • ✅ build/module/Std.Data.HashMap.RawLemmas//instructions: -5.4G (-4.68%)

Medium changes (5✅, 1🟥)

  • ✅ build/module/Init.Data.BitVec.Lemmas//instructions: -1.3G (-1.04%)
  • ✅ build/module/Init.Data.Nat.ToString//instructions: -4.4G (-14.78%) (reduced significance based on absolute threshold)
  • ✅ build/module/Init.Data.Vector.Lemmas//instructions: -1.5G (-3.28%) (reduced significance based on absolute threshold)
  • 🟥 elab/big_match_nat_split//instructions: +110.1M (+1.01%)
  • ✅ elab/grind_bitvec2//instructions: -1.0G (-0.58%)
  • ✅ misc/import Init.Data.BitVec.Lemmas//instructions: -1.2G (-1.08%)

Small changes (34✅, 9🟥)

Too many entries to display here. View the full report on radar instead.

@github-actions github-actions Bot added toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN labels May 11, 2026
@leanprover-bot leanprover-bot added the builds-manual CI has verified that the Lean Language Reference builds against this PR label May 11, 2026
@leanprover-bot
Copy link
Copy Markdown
Collaborator

leanprover-bot commented May 11, 2026 •
edited
Loading

Reference manual CI status:

@mathlib-lean-pr-testing mathlib-lean-pr-testing Bot added the breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan label May 11, 2026
@mathlib-lean-pr-testing
Copy link
Copy Markdown

mathlib-lean-pr-testing Bot commented May 11, 2026 •
edited
Loading

Mathlib CI status (docs):

@datokrat
Copy link
Copy Markdown
Contributor Author

datokrat commented May 11, 2026

!radar

@leanprover-radar
Copy link
Copy Markdown

leanprover-radar commented May 11, 2026 •
edited
Loading

Benchmark results for 63f5f11 against a71f158 are in. There are significant results. @datokrat

  • 🟥 build//instructions: +81.6G (+0.71%)

Large changes (4🟥)

  • 🟥 build/module/Std.Data.HashMap.RawLemmas//instructions: +39.7G (+34.22%)
  • 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Expr//instructions: +14.3G (+22.44%)
  • 🟥 build/module/Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Mul//instructions: +9.1G (+41.21%)
  • 🟥 build/profile/let-to-have transformation//wall-clock: +3s (+52.42%)

Medium changes (5✅, 16🟥)

Too many entries to display here. View the full report on radar instead.

Small changes (75✅, 41🟥)

Too many entries to display here. View the full report on radar instead.

mathlib-nightly-testing Bot pushed a commit to leanprover-community/batteries that referenced this pull request May 11, 2026
Update lean-toolchain for leanprover/lean4#13702
89df553
mathlib-nightly-testing Bot pushed a commit to leanprover-community/mathlib4-nightly-testing that referenced this pull request May 11, 2026
Update lean-toolchain for leanprover/lean4#13702
625cc42
leanprover-bot added a commit to leanprover/reference-manual that referenced this pull request May 11, 2026
@leanprover-bot
Update lean-toolchain for leanprover/lean4#13702
4160f68
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@hargoniX hargoniX Awaiting requested review from hargoniX hargoniX will be requested when the pull request is marked ready for review hargoniX is a code owner

Assignees

No one assigned

Labels

breaks-mathlib This is not necessarily a blocker for merging: but there needs to be a plan builds-manual CI has verified that the Lean Language Reference builds against this PR mathlib4-nightly-available A branch for this PR exists at leanprover-community/mathlib4-nightly-testing:lean-pr-testing-NNNN toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@datokrat @leanprover-radar @leanprover-bot