This PR improves metavariable pretty printing and their hovers in the
InfoView. The hovers in the InfoView now include information about
specific metavariables — it includes information such as the kind of the
metavariable, whether it is a blocked delayed assignment and which
metavariables it is blocked on, and the differences in what variables
exist the metavariable's local context. Additionally, named
metavariables now pretty print with tombstones if they are inaccessible.
Delayed assignment pretty printing now more reliably follows chains of
assignments to find the pending metavariable.
**Example hovers**
Hovering over a natural metavariable:
> `?m.7 : Sort ?u.14`
> A metavariable representing an expression that should be solved for by
unification during the elaboration process. They are created during
elaboration as placeholders for implicit arguments and by `_`
placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`
Hovering over `?baz`, a tactic goal:
> `?baz : ∀ (a : ?m.7) (a : ?m.8), True`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> Variables absent from this metavariable's local context: `a`, `b`, `y`
Hovering over `?refine_1`, which appears under a binder:
> `?m.4 x : Nat`
> A metavariable representing a tactic goal or an expression whose
elaboration is still pending. They usually act like constants until they
are completely solved for. They can be created using `?_` and `?n`
synthetic placeholder syntax.
>
> This metavariable appears here via a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context.
>
> Additional variable in this metavariable's local context: `x`
Hovering over `?m.4`:
> `?m.4 : Nat → Nat`
> Part of the encoding of the *delayed assignment* mechanism. Represents
the metavariable `?refine_1`, which has additional local context
variables. Substitution is delayed until the metavariable's value
contains no metavariables, since all occurrences of the variables from
its local context will need to be replaced with expressions that are
valid in the current context.
>
> Additional variable in this metavariable's local context: `x`
The middle paragraph for `?refine_1` when it has been partially
assigned:
> This metavariable has been assigned, but it is a *delayed assignment*.
Substitution is delayed until the metavariable's value contains no
metavariables, since all occurrences of the variables from its local
context will need to be replaced with expressions that are valid in the
current context. Substitution is awaiting assignment of the following
metavariable: `?foo`
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/474.lean.expected.out (Browse further)
