chore: upstream run_cmd and fixes bugs (#3324)

Co-authored-by: Scott Morrison <scott.morrison@gmail.com>

src/Init/Notation.lean

@@ -464,6 +464,14 @@ macro "without_expected_type " x:term : term => `(let aux := $x; aux)
 
 namespace Lean
 
+/--
+* The `by_elab doSeq` expression runs the `doSeq` as a `TermElabM Expr` to
+  synthesize the expression.
+* `by_elab fun expectedType? => do doSeq` receives the expected type (an `Option Expr`)
+  as well.
+-/
+syntax (name := byElab) "by_elab " doSeq : term
+
 /--
 Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer.
 The only accepted parser for this category is an antiquotation.
@@ -498,3 +506,27 @@ a string literal with the contents of the file at `"parent_dir" / "path" / "to"
 file cannot be read, elaboration fails.
 -/
 syntax (name := includeStr) "include_str " term : term
+
+/--
+The `run_cmd doSeq` command executes code in `CommandElabM Unit`.
+This is almost the same as `#eval show CommandElabM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+-/
+syntax (name := runCmd) "run_cmd " doSeq : command
+
+/--
+The `run_elab doSeq` command executes code in `TermElabM Unit`.
+This is almost the same as `#eval show TermElabM Unit from do doSeq`,
+except that it doesn't print an empty diagnostic.
+-/
+syntax (name := runElab) "run_elab " doSeq : command
+
+/--
+The `run_meta doSeq` command executes code in `MetaM Unit`.
+This is almost the same as `#eval show MetaM Unit from do doSeq`,
+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))

src/Init/Tactics.lean

@@ -941,6 +941,9 @@ syntax (name := repeat1') "repeat1' " tacticSeq : tactic
 syntax "and_intros" : tactic
 macro_rules | `(tactic| and_intros) => `(tactic| repeat' refine And.intro ?_ ?_)
 
+/-- The `run_tac doSeq` tactic executes code in `TacticM Unit`. -/
+syntax (name := runTac) "run_tac " doSeq : tactic
+
 end Tactic
 
 namespace Attr

src/Lean/Elab/BuiltinCommand.lean

@@ -704,6 +704,24 @@ unsafe def elabEvalUnsafe : CommandElab
 @[builtin_command_elab «eval», implemented_by elabEvalUnsafe]
 opaque elabEval : CommandElab
 
+@[builtin_command_elab runCmd]
+def elabRunCmd : CommandElab
+  | `(run_cmd $elems:doSeq) => do
+    ← liftTermElabM <| Term.withDeclName `_run_cmd <|
+      unsafe Term.evalTerm (CommandElabM Unit)
+        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
+        (← `(discard do $elems))
+  | _ => throwUnsupportedSyntax
+
+@[builtin_command_elab runElab]
+def elabRunElab : CommandElab
+  | `(run_elab $elems:doSeq) => do
+    ← liftTermElabM <| Term.withDeclName `_run_elab <|
+      unsafe Term.evalTerm (CommandElabM Unit)
+        (mkApp (mkConst ``CommandElabM) (mkConst ``Unit))
+        (← `(Command.liftTermElabM <| discard do $elems))
+  | _ => throwUnsupportedSyntax
+
 @[builtin_command_elab «synth»] def elabSynth : CommandElab := fun stx => do
   let term := stx[1]
   withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_synth_cmd do

src/Lean/Elab/BuiltinNotation.lean

@@ -7,8 +7,9 @@ import Lean.Compiler.BorrowedAnnotation
 import Lean.Meta.KAbstract
 import Lean.Meta.Closure
 import Lean.Meta.MatchUtil
-import Lean.Elab.SyntheticMVars
 import Lean.Compiler.ImplementedByAttr
+import Lean.Elab.SyntheticMVars
+import Lean.Elab.Eval
 
 namespace Lean.Elab.Term
 open Meta
@@ -427,12 +428,6 @@ private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Ex
   let e ← elabTerm stx[1] expectedType?
   return DiscrTree.mkNoindexAnnotation e
 
--- TODO: investigate whether we need this function
-private def mkAuxNameForElabUnsafe (hint : Name) : TermElabM Name :=
-  withFreshMacroScope do
-    let name := (← getDeclName?).getD Name.anonymous ++ hint
-    return addMacroScope (← getMainModule) name (← getCurrMacroScope)
-
 @[builtin_term_elab «unsafe»]
 def elabUnsafe : TermElab := fun stx expectedType? =>
   match stx with
@@ -443,7 +438,7 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     let t ← mkAuxDefinitionFor (← mkAuxName `unsafe) t
     let .const unsafeFn unsafeLvls .. := t.getAppFn | unreachable!
     let .defnInfo unsafeDefn ← getConstInfo unsafeFn | unreachable!
-    let implName ← mkAuxNameForElabUnsafe `impl
+    let implName ← mkAuxName `unsafe_impl
     addDecl <| Declaration.defnDecl {
       name        := implName
       type        := unsafeDefn.type
@@ -456,4 +451,20 @@ def elabUnsafe : TermElab := fun stx expectedType? =>
     return mkAppN (Lean.mkConst implName unsafeLvls) t.getAppArgs
   | _ => throwUnsupportedSyntax
 
+/-- Elaborator for `by_elab`. -/
+@[builtin_term_elab byElab] def elabRunElab : TermElab := fun stx expectedType? =>
+  match stx with
+  | `(by_elab $cmds:doSeq) => do
+    if let `(Lean.Parser.Term.doSeq| $e:term) := cmds then
+      if e matches `(Lean.Parser.Term.doSeq| fun $[$_args]* => $_) then
+        let tac ← unsafe evalTerm
+          (Option Expr → TermElabM Expr)
+          (Lean.mkForall `x .default
+            (mkApp (Lean.mkConst ``Option) (Lean.mkConst ``Expr))
+            (mkApp (Lean.mkConst ``TermElabM) (Lean.mkConst ``Expr))) e
+        return ← tac expectedType?
+    (← unsafe evalTerm (TermElabM Expr) (mkApp (Lean.mkConst ``TermElabM) (Lean.mkConst ``Expr))
+      (← `(do $cmds)))
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Term

src/Lean/Elab/Eval.lean

@@ -9,7 +9,7 @@ import Lean.Elab.SyntheticMVars
 namespace Lean.Elab.Term
 open Meta
 
-unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := do
+unsafe def evalTerm (α) (type : Expr) (value : Syntax) (safety := DefinitionSafety.safe) : TermElabM α := withoutModifyingEnv do
   let v ← elabTermEnsuringType value type
   synthesizeSyntheticMVarsNoPostponing
   let v ← instantiateMVars v

src/Lean/Elab/Tactic/BuiltinTactic.lean

@@ -9,6 +9,7 @@ import Lean.Meta.Tactic.Contradiction
 import Lean.Meta.Tactic.Refl
 import Lean.Elab.Binders
 import Lean.Elab.Open
+import Lean.Elab.Eval
 import Lean.Elab.SetOption
 import Lean.Elab.Tactic.Basic
 import Lean.Elab.Tactic.ElabTerm
@@ -496,4 +497,11 @@ where
       liftMetaTactic1 (·.tryClearMany toClear)
   | _ => throwUnsupportedSyntax
 
+@[builtin_tactic runTac] def evalRunTac : Tactic := fun stx => do
+  match stx with
+  | `(tactic| run_tac $e:doSeq) =>
+    ← unsafe Term.evalTerm (TacticM Unit) (mkApp (Lean.mkConst ``TacticM) (Lean.mkConst ``Unit))
+      (← `(discard do $e))
+  | _ => throwUnsupportedSyntax
+
 end Lean.Elab.Tactic

tests/lean/1021.lean.expected.out

@@ -1,8 +1,8 @@
-some { range := { pos := { line := 191, column := 42 },
+some { range := { pos := { line := 192, column := 42 },
              charUtf16 := 42,
-             endPos := { line := 197, column := 31 },
+             endPos := { line := 198, column := 31 },
              endCharUtf16 := 31 },
-  selectionRange := { pos := { line := 191, column := 46 },
+  selectionRange := { pos := { line := 192, column := 46 },
                       charUtf16 := 46,
-                      endPos := { line := 191, column := 58 },
+                      endPos := { line := 192, column := 58 },
                       endCharUtf16 := 58 } }

tests/lean/run/run_cmd.lean

@@ -0,0 +1,13 @@
+import Lean
+open Lean Elab Tactic
+
+run_cmd logInfo m!"hello world"
+
+run_cmd unsafe do logInfo "!"
+
+example : True := by
+  run_tac
+    evalApplyLikeTactic MVarId.apply (← `(True.intro))
+
+example : True := by_elab
+  Term.elabTerm (← `(True.intro)) none