import Lean
import Playground.Zulip.EnvExInit

open Lean Meta Elab Command Tactic

error: unsolved goals ⊢ 1 + 2 = 3

-- v4.32: running `Proof` in an async context now emits a `mainOnly`-extension panic as an
-- `info` message with a platform-dependent backtrace; drop info messages, keep checking errors.
#guard_msgs
Error: ❌️ Docstring on `#guard_msgs` does not match generated message:

-
+ error: unsolved goals
+ ⊢ 1 + 2 = 3
 (drop info, check error) in
theorem 
foo: 1 + 2 = 3
foo : 
1: Nat
1 + 
2: Nat
2 = 
3: Nat
3 := by
Error: unsolved goals
⊢ 1 + 2 = 3
1 + 2 = 3
  Proof "trivial":
    rfl
Error: unsolved goals
⊢ 1 + 2 = 3
1 + 2 = 3