From 107763a506772d9fcc294fb536d24d5fce02dbab Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Mon, 20 Apr 2015 15:50:37 -0700
Subject: [PATCH] fix(frontends/lean): better error message for 'proof ... qed'
 blocks containing unsolved placeholders

---
 src/frontends/lean/builtin_exprs.cpp          |  2 +-
 tests/lean/unsolved_proof_qed.lean            |  6 +++
 .../lean/unsolved_proof_qed.lean.expected.out | 43 +++++++++++++++++++
 3 files changed, 50 insertions(+), 1 deletion(-)
 create mode 100644 tests/lean/unsolved_proof_qed.lean
 create mode 100644 tests/lean/unsolved_proof_qed.lean.expected.out

diff --git a/src/frontends/lean/builtin_exprs.cpp b/src/frontends/lean/builtin_exprs.cpp
index b346459fa..098f3b166 100644
--- a/src/frontends/lean/builtin_exprs.cpp
+++ b/src/frontends/lean/builtin_exprs.cpp
@@ -278,7 +278,7 @@ static expr parse_begin_end(parser & p, unsigned, expr const *, pos_info const &
 static expr parse_proof_qed_core(parser & p, pos_info const & pos) {
     expr r = p.parse_expr();
     p.check_token_next(get_qed_tk(), "invalid proof-qed, 'qed' expected");
-    r      = p.mk_by(p.mk_app(get_rexact_tac_fn(), r, pos), pos);
+    r      = p.mk_by(p.mk_app(get_exact_tac_fn(), r, pos), pos);
     return r;
 }
 
diff --git a/tests/lean/unsolved_proof_qed.lean b/tests/lean/unsolved_proof_qed.lean
new file mode 100644
index 000000000..57dcb8dc2
--- /dev/null
+++ b/tests/lean/unsolved_proof_qed.lean
@@ -0,0 +1,6 @@
+example (a b c : nat) (H₁ : a = b) (H₂ : b = c) : a = c :=
+proof eq.trans H₁ _ qed
+
+example (a b c : nat) (H₁ : a = b) (H₂ : b = c) : a = c :=
+have aux : c = a, proof eq.trans _ (eq.symm H₁) qed,
+(eq.symm aux)
diff --git a/tests/lean/unsolved_proof_qed.lean.expected.out b/tests/lean/unsolved_proof_qed.lean.expected.out
new file mode 100644
index 000000000..271da0058
--- /dev/null
+++ b/tests/lean/unsolved_proof_qed.lean.expected.out
@@ -0,0 +1,43 @@
+unsolved_proof_qed.lean:2:18: error: don't know how to synthesize placeholder
+a b c : nat,
+H₁ : a = b,
+H₂ : b = c
+⊢ b = c
+unsolved_proof_qed.lean:2:0: error:invalid 'exact' tactic, term still contains metavariables after elaboration
+  eq.trans H₁ ?M_1
+proof state:
+a b c : nat,
+H₁ : a = b,
+H₂ : b = c
+⊢ a = c
+unsolved_proof_qed.lean:2:0: error: don't know how to synthesize placeholder
+a b c : nat,
+H₁ : a = b,
+H₂ : b = c
+⊢ a = c
+unsolved_proof_qed.lean:2:0: error: failed to add declaration '14.0' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b c : nat) (H₁ : …) (H₂ : …),
+    ?M_1
+unsolved_proof_qed.lean:5:33: error: don't know how to synthesize placeholder
+a b c : nat,
+H₁ : a = b,
+H₂ : b = c
+⊢ c = b
+unsolved_proof_qed.lean:5:18: error:invalid 'exact' tactic, term still contains metavariables after elaboration
+  eq.trans ?M_1 (eq.symm H₁)
+proof state:
+a b c : nat,
+H₁ : a = b,
+H₂ : b = c
+⊢ c = a
+unsolved_proof_qed.lean:5:18: error: don't know how to synthesize placeholder
+a b c : nat,
+H₁ : a = b,
+H₂ : b = c
+⊢ c = a
+unsolved_proof_qed.lean:5:0: error: failed to add declaration '14.1' to environment, value has metavariables
+remark: set 'formatter.hide_full_terms' to false to see the complete term
+  λ (a b c : nat) (H₁ : …) (H₂ : …),
+    have aux : …, from ?M_1,
+    …