From d0f6bbdf02d5eb03f704e183b1ddf1f7dad08bfe Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 23 Aug 2018 13:32:25 -0700
Subject: [PATCH] chore(tests/lean): replace `run_cmd` with `#eval`

---
 tests/lean/macro1.lean              | 8 ++++----
 tests/lean/macro1.lean.expected.out | 2 --
 tests/lean/trace1.lean              | 2 +-
 3 files changed, 5 insertions(+), 7 deletions(-)

diff --git a/tests/lean/macro1.lean b/tests/lean/macro1.lean
index 04724833e7..4cbeb0b877 100644
--- a/tests/lean/macro1.lean
+++ b/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⟩
 ]⟩
diff --git a/tests/lean/macro1.lean.expected.out b/tests/lean/macro1.lean.expected.out
index d905341f21..92cff6e943 100644
--- a/tests/lean/macro1.lean.expected.out
+++ b/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)))
diff --git a/tests/lean/trace1.lean b/tests/lean/trace1.lean
index 4d18330160..b0ceb3fd29 100644
--- a/tests/lean/trace1.lean
+++ b/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 "---",