chore: turn on new do elaborator in Core

[sgraf812]

This PR turns on the new do elaborator in Init, Lean, Std, Lake and the testsuite.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 78682df against e7e3588 are in! @sgraf812

• ✅ build//instructions: -353.9G (-2.81%)

Large changes (2✅)

• ✅ build/module/Lean.Meta.Tactic.FunInd//instructions: -13.3G (-17.24%)
• ✅ build/module/Lean.Meta.Tactic.Grind.EMatch//instructions: -5.1G (-6.68%)

Medium changes (79✅, 1🟥)

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

Small changes (837✅, 17🟥)

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

[sgraf812]

I looked into the only reported medium regression in #12656 (comment): ~+20% more instructions in Lean/Meta/Match/Rewrite.lean. It's not related to the do elaborator; it's LCNF taking more time, presumably to simplify away the EarlyReturnT layer. I'm inclined to accept.

[Rob23oba]

It's a bit unfortunate that there have to be so many adaptations regarding do match. But why exactly do do matches have to be completely non-dependent by default? Shouldn't it be enough to make them non-generalizing, i.e. not affect the return type or the local context? I don't see a reason why the type of h shouldn't be i+1 <= as.size in

let rec loop (i : Nat) (h : i ≤ as.size) (b : β) : m β := do
    match i, h with
    | 0,   _ => pure b
    | i+1, h =>

Edit: Nice to see some good performance wins, though!

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase cd7f55b6c92b6d20fb2a0428abc097fa8be421b3 --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 11:53:09)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c1ab1668b236d00b4cd61a4fa83b5516b705afdd --onto ed0fd1e933239beaa7aaa12598f961c260062ab6. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-24 17:10:01)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase cd7f55b6c92b6d20fb2a0428abc097fa8be421b3 --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-24 11:53:11)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c1ab1668b236d00b4cd61a4fa83b5516b705afdd --onto 8038a8b8904f89ad9542c8eda11379f8f006eab1. You can force reference manual CI using the force-manual-ci label. (2026-02-24 17:10:03)
• ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-03-05 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-03-09 11:40:22)

[sgraf812]

I don't see a reason why the type of h shouldn't be i+1 <= as.size in

That's actually a good point. I opened #12673.

[Rob23oba]

I'm not entirely sure why all of these changes are necessary, can you explain?

[Rob23oba]

Also, is it planned that we get ForInNew eventually? It'd be cool to have this work (or more importantly, the equivalent with withLocalDecl):

Example where it would be really nice to have ForInNew

import Lean

set_option backward.do.legacy false

open Lean Meta Elab Term
elab tk:"with_cont " fn:term : doElem <= dec => do
  let combinator ← elabTerm fn none
  let type ← inferType combinator
  let .forallE _ t b _ ← whnfForall type | throwFunctionExpected combinator
  let u := (← read).monadInfo.u
  let cont ← withLetDecl dec.resultName (.const ``PUnit [u.succ]) (.const ``PUnit.unit [u.succ]) fun e => do
    mkLetFVars #[e] (← dec.k)
  let contTy ← inferType cont
  unless ← isDefEq t contTy do
    throwErrorAt tk "error"
  let res := (← read).doBlockResultType
  let monad := (← read).monadInfo.m
  let expect := .app monad res
  unless ← isDefEq b expect do
    throwErrorAt tk "other error"
  return combinator.beta #[cont]

@[doElem_control_info doElemWith_cont_]
def controlInfoWithCont : Do.ControlInfoHandler := fun _ => pure .pure

def test (n : Nat) : ReaderM Nat Nat := do
  for i in *...n do
    with_cont withReader (· + 1)
  read

#guard ((test 0).run 3).run == 3
#guard ((test 5).run 3).run == 8 -- fails :-(

[sgraf812]

Yes, I agree that ForInNew is cool and The Right Way To Do It. Unfortunately, it is blocked on the compiler properly eliminating tail calls in all the loops we might want to generate. We decided that it's best to stay with ForIn for now to have a reliable system.

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for a922d86 against 333ab1c are in! @sgraf812

• ✅ build//instructions: -338.9G (-2.66%)

Large changes (3✅)

• ✅ build//instructions: -338.9G (-2.66%)
• ✅ build/module/Lean.Meta.Tactic.FunInd//instructions: -13.3G (-17.34%)
• ✅ build/module/Lean.Meta.Tactic.Grind.EMatch//instructions: -5.1G (-6.72%)

and 1 hidden

Medium changes (75✅, 1🟥)

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

Small changes (818✅, 24🟥)

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

[Rob23oba]

Thanks, good to see the new do elaborator moving forward. One small question but otherwise everything LGTM. (also I just wanted to mention that I got one function from 7.5s elaboration time to 1s using the new do elaborator!)

[sgraf812]

Thanks, good to see the new do elaborator moving forward. One small question but otherwise everything LGTM. (also I just wanted to mention that I got one function from 7.5s elaboration time to 1s using the new do elaborator!)

Great! Thanks for the review and the benchmark :) Will merge once Mathlib reports back in green

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ✅ Mathlib branch lean-pr-testing-12656 has successfully built against this PR. (2026-03-09 12:36:25) View Log