Zulip Chat Archive

Stream: lean4

Topic: PANIC at ... : unknown metavariable

Michael Stoll (Jun 08 2025 at 20:26):

While working on a file in VSCode (Lean4 VS Code Extension v0.0.206, Lean v4.20.0), I keep seeing messages of the form

PANIC at Lean.MetavarContext.getLevelDepth Lean.MetavarContext:874:14: unknown metavariable

in a pop-up window. The backtrace is rather long and begins like this:

backtrace

Is this a known problem?

Aaron Liu (Jun 08 2025 at 20:47):

Can you provide a #mwe?

Michael Stoll (Jun 08 2025 at 20:48):

Not right now (I've finished working and will go to bed...).
It seems to occur while typing; maybe it tries to make sense of some partially typed thing, which triggers the error.

Jovan Gerbscheid (Jun 08 2025 at 23:32):

That's the same error as reported in #mathlib4 > ✔ Crash in `sup`/`inf` / `max`/`min` delaborators.

It means that there is a universe level metavariable in an expression that isn't in the metavariable context. That particular case was fixed by a PR I did to lean, meaning that it would be fixed in v4.21.0. Did your example by any chance involve the max or min function and a rewrite tactic?

Michael Stoll (Jun 09 2025 at 09:03):

Jovan Gerbscheid said:

Did your example by any chance involve the max or min function and a rewrite tactic?

That's very well possible; the proof I was working on involves Finset.sup' and also max. Rewrites occur in the proof. But just stepping through the finished proof does not produce the PANIC; I'm quite positive that it happened while editing.

Jovan Gerbscheid (Jun 09 2025 at 12:12):

The error should only appear when the cursor is on a lemma that involves max, within a rewrite tactic.

Aaron Liu (Jun 09 2025 at 12:15):

I can't tell if it's the same problem with only the first part of the trace

Aaron Liu (Jun 09 2025 at 12:15):

but it certainly looks similar

Michael Stoll (Jun 10 2025 at 18:08):

It just occurred again, when I put the cursor right before the ] in rw [this.map_max], so it really looks like it is the same error.

Last updated: Dec 20 2025 at 21:32 UTC