feat(frontends/lean): automatically add 'info' tactic in begin-end blocks

Actually, the tactic is only added when Lean is in collect-info mode.

src/frontends/lean/builtin_exprs.cpp

@@ -26,6 +26,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/extra_info.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/tokens.h"
+#include "frontends/lean/info_tactic.h"
 
 namespace lean {
 namespace notation {
@@ -142,10 +143,16 @@ static expr parse_begin_end_core(parser & p, pos_info const & pos) {
     parser::no_undef_id_error_scope scope(p);
     environment env = open_tactic_namespace(p);
     while (!p.curr_is_token(get_end_tk())) {
-        if (first)
+        if (first) {
             first = false;
-        else
+        } else {
+            auto pos = p.pos();
             p.check_token_next(get_comma_tk(), "invalid 'begin-end' expression, ',' expected");
+            if (p.collecting_info()) {
+                expr info_tac = p.save_pos(mk_info_tactic_expr(), pos);
+                tacs.push_back(info_tac);
+            }
+        }
         if (p.curr_is_token(get_end_tk()))
             break;
         bool use_exact = (p.curr_is_token(get_have_tk()) || p.curr_is_token(get_show_tk()) ||

src/frontends/lean/info_tactic.cpp

@@ -41,8 +41,14 @@ tactic mk_info_tactic(elaborate_fn const & fn, expr const & e) {
         });
 }
 
+#define INFO_TAC_NAME name({"tactic", "info"})
+
+expr mk_info_tactic_expr() {
+    return mk_constant(INFO_TAC_NAME);
+}
+
 void initialize_info_tactic() {
-    register_tac(name({"tactic", "info"}),
+    register_tac(INFO_TAC_NAME,
                  [](type_checker &, elaborate_fn const & fn, expr const & e, pos_info_provider const *) {
                      return mk_info_tactic(fn, e);
                  });

src/frontends/lean/info_tactic.h

@@ -8,6 +8,7 @@ Author: Leonardo de Moura
 #include "library/tactic/proof_state.h"
 
 namespace lean {
+expr mk_info_tactic_expr();
 /** \brief The tactic framework does not have access to the info manager.
     Thus, it cannot store the proof_state there. The info tactic accomplishes
     that by (temporarily) saving the proof state in a thread-local storage

tests/lean/interactive/proof_state_info2.input

@@ -0,0 +1,15 @@
+VISIT proof_state_info.lean
+SYNC 9
+import logic
+open tactic
+theorem tst (a b c : Prop) : a → b → a ∧ b :=
+begin
+  intros (Ha, Hb),
+  apply and.intro,
+  apply Ha,
+  apply Hb,
+end
+WAIT
+INFO 5 17
+INFO 6 17
+INFO 7 10

tests/lean/interactive/proof_state_info2.input.expected.out

@@ -0,0 +1,27 @@
+-- BEGINWAIT
+-- ENDWAIT
+-- BEGININFO
+-- TYPE|5|17
+tactic
+-- ACK
+-- PROOF_STATE|5|17
+a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ a ∧ b
+-- ACK
+-- ENDINFO
+-- BEGININFO
+-- TYPE|6|17
+tactic
+-- ACK
+-- PROOF_STATE|6|17
+a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ a
+a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ b
+-- ACK
+-- ENDINFO
+-- BEGININFO
+-- TYPE|7|10
+tactic
+-- ACK
+-- PROOF_STATE|7|10
+a : Prop, b : Prop, c : Prop, Ha : a, Hb : b ⊢ b
+-- ACK
+-- ENDINFO