This PR improves pretty printing of level metavariables: they now print
with a per-definition index rather than their per-module internal
identifiers. Furthermore, `+` is printed uniformly in level expressions
with surrounding spaces. **Breaking metaprogramming change:** level
pretty printing should use `delabLevel` or `MessageData.ofLevel`;
functions such as `format` or `toString` do not have access to the
indices, since they are stored in the current metacontext. Absent index
information, metavariables print with the raw internal identifier as
`?_mvar.nnn`. **Note:** The heartbeat counter also increases quicker due
to counting allocations that record level metavariable indices. In some
tests we needed to increase `maxHeartbeats` by 20–50% to compensate,
without a corresponding slowdown.
This PR adds a warning to any `def` of class type that does not also
declare an appropriate reducibility.
The warning check runs after elaboration (checking the actual
reducibility status via `getReducibilityStatus`) rather than
syntactically checking modifiers before elaboration. This is necessary
to accommodate patterns like `@[to_additive (attr :=
implicit_reducible)]` in Mathlib, where the reducibility attribute is
applied during `.afterCompilation` by another attribute, and would be
missed by a purely syntactic check.
---------
Co-authored-by: Paul Reichert <6992158+datokrat@users.noreply.github.com>
Co-authored-by: Kim Morrison <kim@tqft.net>
Co-authored-by: Claude Opus 4.6 <noreply@anthropic.com>
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.
2026-02-25 13:51:53 +00:00
Renamed from tests/lean/run/methodSpecs.lean (Browse further)
