feat: new, extensible do elaborator

[sgraf812]

This PR adds a new, extensible do elaborator. Users can opt into the new elaborator by unsetting the option backward.do.legacy.

New elaborators for the builtin doElem syntax category can be registered with attribute doElem_elab. For new syntax, additionally a control info handler must be registered with attribute doElem_control_info that specifies whether the new syntax returns early, breaks, continues and which mut vars it reassigns.

Do elaborators have type TSyntax `doElem → DoElemCont → DoElabM Expr, where DoElabM is essentially TermElabM and the DoElemCont represents how the rest of the do block is to be elaborated. Consult the docstrings for more details.

Breaking Changes:

• The syntax for let pat := rhs | otherwise and similar now scope over the doSeq that follows. Furthermore, otherwise and the sequence that follows are now doSeqIndented in order not to steal syntax from record syntax.

Breaking Changes when opting into new elaborator by unsetting backward.do.legacy:

• do notation now always requires Pure.
• do match is now always non-dependent. There is do match (dependent := true) that expands to a
  term match as a workaround for some dependent uses.

[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 818a0ec6a74d6b9db984e197a1a959e5c540b682 --onto 4cdc199f772977113bd6c1bf87a6c02b78d5c4d3. You can force Mathlib CI using the force-mathlib-ci label. (2026-02-12 18:28:07)

[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 818a0ec6a74d6b9db984e197a1a959e5c540b682 --onto 03dc334f73259e1bae0b8f2b80a39a82e1de3df6. You can force reference manual CI using the force-manual-ci label. (2026-02-12 18:28:10)