From 834375a042263bfa4d66ef10a1c9fcbf4232e0ac Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 31 May 2017 16:07:08 +0200 Subject: [PATCH] fix(library/eval_helper): evaluating tactics --- src/library/eval_helper.cpp | 2 +- tests/lean/eval_tactic.lean | 2 ++ tests/lean/eval_tactic.lean.expected.out | 2 ++ 3 files changed, 5 insertions(+), 1 deletion(-) create mode 100644 tests/lean/eval_tactic.lean create mode 100644 tests/lean/eval_tactic.lean.expected.out diff --git a/src/library/eval_helper.cpp b/src/library/eval_helper.cpp index e3c43d08b7..fc19f352ed 100644 --- a/src/library/eval_helper.cpp +++ b/src/library/eval_helper.cpp @@ -67,7 +67,7 @@ optional eval_helper::try_exec_io() { optional eval_helper::try_exec_tac() { if (is_constant(get_app_fn(m_ty), get_tactic_name())) { auto tac_st = mk_tactic_state_for(m_env, m_opts, m_fn, m_tc.mctx(), m_tc.lctx(), mk_true()); - m_vms.push(tactic::to_obj(tac_st)); + m_args.push_back(tactic::to_obj(tac_st)); auto r = invoke_fn(); if (tactic::is_result_success(r)) { return optional(tactic::get_result_value(r)); diff --git a/tests/lean/eval_tactic.lean b/tests/lean/eval_tactic.lean new file mode 100644 index 0000000000..34c81e1e10 --- /dev/null +++ b/tests/lean/eval_tactic.lean @@ -0,0 +1,2 @@ +#eval tactic.trace 42 +#eval (tactic.fail "nope" : tactic nat) diff --git a/tests/lean/eval_tactic.lean.expected.out b/tests/lean/eval_tactic.lean.expected.out new file mode 100644 index 0000000000..f7fe767e96 --- /dev/null +++ b/tests/lean/eval_tactic.lean.expected.out @@ -0,0 +1,2 @@ +42 +eval_tactic.lean:2:0: error: nope