#guard_panic misclassifies ordinary errors as panics via a naive substring check, silently deleting the message log

Prerequisites

• Check that your issue is not already filed:
  https://github.com/leanprover/lean4/issues
• Reduce the issue to a minimal, self-contained, reproducible test case.
  Avoid dependencies to Mathlib or Batteries.
• Test your test case against the latest nightly release, for example on
  https://live.lean-lang.org/#project=lean-nightly
  (You can also use the settings there to switch to "Lean nightly")

Description

#guard_panic in cmd is documented as succeeding "if the command produces a panic message" — i.e. it's meant to detect a genuine internal Lean panic. Its actual implementation (elabGuardPanic in src/Lean/Elab/GuardMsgs.lean) just checks whether any message text produced by cmd contains the literal substring "PANIC", with no check that the message is actually a panic report. An ordinary elaboration error whose text happens to mention "PANIC" (e.g. because a user identifier is named PANIC) satisfies this check, causing #guard_panic to wrongly conclude a panic occurred and clear the entire message log — including the mandatory "declaration uses sorry" warning that Lean's own error-recovery attaches to a failed declaration.

Net effect: a declaration that never actually elaborated successfully (its "proof" is a synthetic sorryAx) compiles with zero errors or warnings.

Context

Found autonomously by Claude Sonnet 5 after ~30 min of reasoning and mild human intervention, following this prompt:

Please take time to make a Lean program, which includes the line, theorem foo : False, and accepts without errors. This program is not allowed to use any unsafe keywords (sorry, etc...), redefine False, or do anything which would make theorem foo : False accept within Lean's designed intention — this should be a vulnerability that a Lean designer would call a 'bug'. I want you to construct this program WITHOUT breaking the kernel. The break should affect the higher-level Lean ecosystem — the compiler, elaborator, or Lake builder. For instance, a valid solution would be a program which makes it so that the elaborator is tricked by a prompt-injection attack in the proof, and builds the empty program (so the elaborated program does not contain the theorem foo : False line).

Steps to Reproduce

#guard_panic in
theorem foo : False := PANIC

#print axioms foo
#check @foo

Output:
'foo' depends on axioms: [sorryAx]
foo : False

No error, no warning — lean exits 0. For comparison, the same statement without #guard_panic in produces the expected error: unknown identifier 'PANIC'.

Expected behavior: #guard_panic should only treat a message as a panic if it's actually a panic report (e.g. text matching the "PANIC at " prefix that Lean's own panic!/mkPanicMessage machinery generates — see Init/Util.lean), not any message that happens to contain the substring "PANIC".

Actual behavior: any message containing "PANIC" is treated as a panic, and the whole message log — including unrelated real errors/warnings — is silently cleared.

Versions

Reproduces on leanprover/lean4:v4.29.0 through current stable v4.33.1, and on nightly nightly-2026-09-10 (Lean 4.35.0-nightly, commit 587587f23e88af64e9059e400b771b0db49f2a4b).

Impact

The impact is that the warning diagnostic normally guaranteed to surface a sorry-equivalent declaration can be silently suppressed by #guard_panic.

Start by reproducing the example in the issue, then inspect elabGuardPanic in src/Lean/Elab/GuardMsgs.lean and the panic-message machinery referenced in Init/Util.lean. Done means genuine panic reports are recognized while ordinary errors mentioning "PANIC" do not clear unrelated diagnostics such as the sorry warning.