feat(frontends/lean): position information in error messages

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/builtin/tactic.lua

@@ -9,6 +9,7 @@ nary_combinator("Then", Then)
 nary_combinator("OrElse", OrElse)
 const_tactic("exact", assumption_tac)
 const_tactic("trivial", trivial_tac)
+const_tactic("id", id_tac)
 const_tactic("absurd", absurd_tac)
 const_tactic("conj_hyp", conj_hyp_tac)
 const_tactic("disj_hyp", disj_hyp_tac)

src/frontends/lean/parser_expr.cpp

@@ -996,7 +996,7 @@ expr parser_imp::parse_show_expr() {
     } else if (curr_is_identifier() && curr_name() == g_from) {
         next();
         expr b = parse_expr();
-        return mk_let(g_H_show, t, b, Var(0));
+        return save(mk_let(g_H_show, t, b, Var(0)), p);
     } else {
         throw parser_error("invalid 'show' expected, 'from' or 'by' expected", p);
     }
@@ -1015,11 +1015,12 @@ expr parser_imp::parse_have_expr() {
     check_comma_next("invalid 'have' expression, ',' expected");
     expr val;
     if (curr() == scanner::token::By) {
+        auto p2 = pos();
         next();
         tactic tac = parse_tactic_expr();
         expr r = mk_placeholder(some_expr(t));
         m_tactic_hints.insert(mk_pair(r, tac));
-        val = save(r, p);
+        val = save(r, p2);
     } else if (curr_is_identifier() && curr_name() == g_from) {
         next();
         val = parse_expr();
@@ -1027,7 +1028,7 @@ expr parser_imp::parse_have_expr() {
     check_comma_next("invalid 'have' expression, ',' expected");
     register_binding(id);
     expr body = parse_expr();
-    return mk_let(id, t, val, body);
+    return save(mk_let(id, t, val, body), p);
 }
 
 /** \brief Parse <tt>'by' tactic</tt> */

src/frontends/lean/parser_tactic.cpp

@@ -83,7 +83,7 @@ expr parser_imp::mk_proof_for(proof_state const & s, pos_info const & p, context
         }
         return pr;
     } else {
-        throw tactic_cmd_error("invalid 'done' command, proof cannot be produced from this state", p, s);
+        throw tactic_cmd_error("failed to create proof for the following proof state", p, s);
     }
 }
 

tests/lean/bad_simp2.lean.expected.out

@@ -4,13 +4,13 @@
   Assumed: f
   Assumed: Ax1
   Proved: T1a
-bad_simp2.lean:14:3: error: invalid 'done' command, proof cannot be produced from this state
+bad_simp2.lean:14:3: error: failed to create proof for the following proof state
 Proof state:
 A : (Type 1) ⊢ f A = A
   Assumed: g
   Assumed: Ax2
   Proved: T2a
-bad_simp2.lean:24:3: error: invalid 'done' command, proof cannot be produced from this state
+bad_simp2.lean:24:3: error: failed to create proof for the following proof state
 Proof state:
 A : Type → (Type 1) ⊢ g A = A Bool
   Assumed: h
@@ -18,13 +18,13 @@ A : Type → (Type 1) ⊢ g A = A Bool
   Proved: T3a
   Assumed: Ax4
   Proved: T4a
-bad_simp2.lean:40:3: error: invalid 'done' command, proof cannot be produced from this state
+bad_simp2.lean:40:3: error: failed to create proof for the following proof state
 Proof state:
 A : Type, B : (Type 1) ⊢ h A B = B
   Assumed: h2
   Assumed: Ax5
   Proved: T5a
-bad_simp2.lean:51:3: error: invalid 'done' command, proof cannot be produced from this state
+bad_simp2.lean:51:3: error: failed to create proof for the following proof state
 Proof state:
 A : Type, B : (Type 1) ⊢ h2 A B = A
 theorem T5a (A B : Type) : h2 A B = A :=

tests/lean/interactive/t1.lean.expected.out

@@ -2,10 +2,10 @@
   Set: pp::unicode
 Proof state:
 a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
-## [stdin]:5:0: error: invalid 'done' command, proof cannot be produced from this state
+## [stdin]:5:0: error: failed to create proof for the following proof state
 Proof state:
 a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
-## [stdin]:6:0: error: invalid 'done' command, proof cannot be produced from this state
+## [stdin]:6:0: error: failed to create proof for the following proof state
 Proof state:
 a : Bool, b : Bool, H : a, H::1 : b ⊢ a ∧ b
 ## [stdin]:7:0: error: unknown tactic 'imp_tac2'

tests/lean/interactive/t10.lean.expected.out

@@ -7,7 +7,7 @@ no goals
 ## Proof state:
 A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
 ## [stdin]:15:3: error: unknown tactic 'simple2_tac'
-## [stdin]:15:16: error: invalid 'done' command, proof cannot be produced from this state
+## [stdin]:15:16: error: failed to create proof for the following proof state
 Proof state:
 A : Bool, B : Bool, H : A ∧ B, H1 : A ⊢ B
 ## Proof state:

tests/lean/j4.lean

@@ -24,11 +24,11 @@ theorem not_prime_eq (n : Nat) (H1 : n ≥ 2) (H2 : ¬ prime n) : ∃ m, m | n
 := have H3 : ¬ n ≥ 2 ∨ ¬ (∀ m : Nat, m | n → m = 1 ∨ m = n),
      from (not_and _ _ ◂ H2),
    have H4 : ¬ ¬ n ≥ 2,
-     from by skip, -- Ignore this hole
+     by skip, -- Ignore this hole
    obtain (m : Nat) (H5 :  ¬ (m | n → m = 1 ∨ m = n)),
      from (not_forall_elim (resolve1 H3 H4)),
    have H6 : m | n ∧ ¬ (m = 1 ∨ m = n),
-     from _,       -- <<< Lean will display the proof state for this hole
+     by id,       -- <<< id is the "do-nothing" tactic, it will fail and Lean will display the proof state for this hole
    have H7 : ¬ (m = 1 ∨ m = n) ↔ (m ≠ 1 ∧ m ≠ n),
      from (not_or (m = 1) (m = n)),
    have H8 : m | n ∧ m ≠ 1 ∧ m ≠ n,

tests/lean/j4.lean.expected.out

@@ -8,7 +8,7 @@
   Proved: dvd_intro
   Proved: dvd_trans
   Defined: prime
-j4.lean:38:0: error: invalid tactic command, unexpected end of file
+j4.lean:31:5: error: failed to create proof for the following proof state
 Proof state:
 n :
     ℕ,