fix: run_meta macro (#3334)

src/Init/Notation.lean

@@ -528,5 +528,4 @@ except that it doesn't print an empty diagnostic.
 
 (This is effectively a synonym for `run_elab`.)
 -/
-macro (name := runMeta) "run_meta " elems:doSeq : command =>
-  `(command| run_elab (show MetaM Unit from do $elems))
+syntax (name := runMeta) "run_meta " doSeq : command

src/Lean/Elab/BuiltinCommand.lean

@@ -704,22 +704,37 @@ unsafe def elabEvalUnsafe : CommandElab
 @[builtin_command_elab «eval», implemented_by elabEvalUnsafe]
 opaque elabEval : CommandElab
 
+private def checkImportsForRunCmds : CommandElabM Unit := do
+  unless (← getEnv).contains ``CommandElabM do
+    throwError "to use this command, include `import Lean.Elab.Command`"
+
 @[builtin_command_elab runCmd]
 def elabRunCmd : CommandElab
   | `(run_cmd $elems:doSeq) => do
-    ← liftTermElabM <| Term.withDeclName `_run_cmd <|
+    checkImportsForRunCmds
+    (← liftTermElabM <| Term.withDeclName `_run_cmd <|
       unsafe Term.evalTerm (CommandElabM Unit)
         (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(discard do $elems))
+        (← `(discard do $elems)))
   | _ => throwUnsupportedSyntax
 
 @[builtin_command_elab runElab]
 def elabRunElab : CommandElab
   | `(run_elab $elems:doSeq) => do
-    ← liftTermElabM <| Term.withDeclName `_run_elab <|
+    checkImportsForRunCmds
+    (← liftTermElabM <| Term.withDeclName `_run_elab <|
       unsafe Term.evalTerm (CommandElabM Unit)
         (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
-        (← `(Command.liftTermElabM <| discard do $elems))
+        (← `(Command.liftTermElabM <| discard do $elems)))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runMeta]
+def elabRunMeta : CommandElab := fun stx =>
+  match stx with
+  | `(run_meta $elems:doSeq) => do
+     checkImportsForRunCmds
+     let stxNew ← `(command| run_elab (show Lean.Meta.MetaM Unit from do $elems))
+     withMacroExpansion stx stxNew do elabCommand stxNew
   | _ => throwUnsupportedSyntax
 
 @[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do

tests/lean/run/run_meta1.lean

@@ -0,0 +1,8 @@
+import Lean.Elab.Command
+
+run_meta guard true
+
+open Lean Meta in
+run_meta do
+  let type ← inferType (mkConst ``true)
+  IO.println type

tests/lean/run_meta1.lean

@@ -0,0 +1 @@
+run_meta guard true

tests/lean/run_meta1.lean.expected.out

@@ -0,0 +1 @@
+run_meta1.lean:1:0-1:19: error: to use this command, include `import Lean.Elab.Command`