chore(tests/lean): replace run_cmd with #eval

tests/lean/macro1.lean

@@ -41,18 +41,18 @@ match (expand' stx >>= resolve').run' cfg () with
 | except.error e := tactic.fail e
 | except.ok stx  := tactic.trace stx
 
-run_cmd test $ syntax.node ⟨`lambda, [
+#eval test $ syntax.node ⟨`lambda, [
   syntax.node ⟨name.anonymous, [syntax.ident ⟨info, `x, none, none⟩]⟩,
   syntax.ident ⟨info, `x, none, none⟩
 ]⟩
 
-run_cmd test $ syntax.node ⟨`lambda, [
+#eval test $ syntax.node ⟨`lambda, [
   syntax.node ⟨name.anonymous, [syntax.ident ⟨info, `x, none, none⟩]⟩,
   syntax.ident ⟨info, `y, none, none⟩
 ]⟩
 
 -- test macro shadowing
-run_cmd test $ syntax.node ⟨`lambda, [
+#eval test $ syntax.node ⟨`lambda, [
   syntax.node ⟨name.anonymous, [syntax.ident ⟨info, `x, none, none⟩]⟩,
   syntax.node ⟨`intro_x, [
     syntax.ident ⟨info, `x, none, none⟩
@@ -60,7 +60,7 @@ run_cmd test $ syntax.node ⟨`lambda, [
 ]⟩
 
 -- test field notation
-run_cmd test $ syntax.node ⟨`lambda, [
+#eval test $ syntax.node ⟨`lambda, [
   syntax.node ⟨name.anonymous, [syntax.ident ⟨info, `x.y, none, none⟩]⟩,
   syntax.ident ⟨info, `x.y.z, none, none⟩
 ]⟩

tests/lean/macro1.lean.expected.out

@@ -1,6 +1,4 @@
 (lambda_core (bind [x] x:0))
 macro1.lean:49:0: error: unknown identifier y
-state:
-⊢ true
 (lambda_core (bind [x] (lambda_core (bind [x!1] x:1))))
 (lambda_core (bind [x.y] x.y.z:0.(z)))

tests/lean/trace1.lean

@@ -15,7 +15,7 @@ trace_root ⟨1, 0⟩ `trace.type_context.is_def_eq "type_context.is_def_eq trac
   ⟩
 ⟩)
 
-run_cmd
+#eval
 do let test opts := tactic.trace $ format.join $ list.intersperse format.line $ (test opts).to_list.map $ λ ⟨pos, tr⟩, to_fmt pos ++ ": " ++ tr.pp,
    test options.mk,
    tactic.trace "---",