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)

[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 04b9496 against c1ab166 are in! @sgraf812

• ✅ build//instructions: -339.4G (-2.69%)

Large changes (2✅)

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

Medium changes (76✅, 1🟥)

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

Small changes (827✅, 25🟥)

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

[Rob23oba]

Huh, seems like putting do at the end of this line and undoing the changes to lines 22-24 fixes the issue (some kind of elaboration order issue? by exact also works btw but is really ugly)