This PR removes the transitional `macro_rules` for `repeat`, `while`,
and `repeat ... until` from `Init.While`. After the latest stage0
update, the `@[builtin_macro]` and `@[builtin_doElem_elab]` definitions
in `Lean.Elab.BuiltinDo.Repeat` are picked up directly, so the bootstrap
duplicates in `Init.While` are no longer needed. `Init.While` now only
provides the `Loop` type and its `ForIn` instance.
This PR also adjusts `repeat`'s `ControlInfo` to match `for ... in`: its
`numRegularExits` is now unconditionally `1` rather than `if info.breaks
then 1 else 0`. Reporting `0` when the body has no `break` causes
`inferControlInfoSeq` (in any enclosing sequence whose `ControlInfo` is
inferred — e.g. a surrounding `for`/`if`/`match`/`try` body) to stop
aggregating after the `repeat` and miss any `return`/`break`/`continue`
that follows. The corresponding elaborator then sees the actual control
flow disagree with the inferred info and throws errors like `Early
returning ... but the info said there is no early return`. The new test
in `tests/elab/newdo.lean` pins down the regression. See
[#13437](https://github.com/leanprover/lean4/pull/13437) for further
discussion.
This PR fixes#12846, where the new do elaborator produced confusing
errors when a do element's continuation had a mismatched monadic result
type. The errors were misleading both in location (e.g., pointing at the
value of `let x ← value` rather than the `let` keyword) and in content
(e.g., mentioning `PUnit.unit` which the user never wrote).
The fix introduces `DoElemCont.ensureUnitAt`/`ensureHasTypeAt`, which
check the continuation result type early and report mismatches with a
clear message ("The `do` element has monadic result type ... but the
rest of the `do` block has monadic result type ..."). Each do-element
elaborator (`let`, `have`, `let rec`, `for`, `unless`, `dbg_trace`,
`assert!`, `idbg`, etc.) now captures its keyword token via `%$tk` and
passes it to `ensureUnitAt` so that the error points at the do element
rather than at an internal elaboration artifact. The old ad-hoc type
check in `for` and the confusing `ensureHasType` call in
`continueWithUnit` are replaced by this uniform mechanism. Additionally,
`extractMonadInfo` now calls `instantiateMVars` on the expected type,
and `While.lean`/`If.lean` macros propagate token info through their
expansions.
Closes#12846
---------
Co-authored-by: Rob23oba <robin.arnez@web.de>
This PR fixes#12768, where the new `do` elaborator produced a
"declaration has free variables" kernel error when the bind
continuation's result type was definitionally but not syntactically
independent of the bound variable. The fix moves creation of the result
type metavariable before `withLocalDecl`, so the unifier must reduce
away the dependency.
For example, given `def Quoted (x : Nat) := Nat`, the expression `do let
val ← pure 3; withStuff val do return 3` would fail because `β` was
assigned `Quoted val` rather than `Nat`.
This PR sets up the new integrated test/bench suite. It then migrates
all benchmarks and some related tests to the new suite. There's also
some documentation and some linting.
For now, a lot of the old tests are left alone so this PR doesn't become
even larger than it already is. Eventually, all tests should be migrated
to the new suite though so there isn't a confusing mix of two systems.
