fix(library/tactic): avoid 'unknown' message in trace_tac when position information is not available

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

src/library/tactic/expr_to_tactic.cpp

@@ -186,7 +186,7 @@ static register_tac reg_state(name(g_tac, "state"), [](type_checker &, expr cons
         if (p)
             return trace_state_tactic(std::string(p->get_file_name()), p->get_pos_info(e));
         else
-            return trace_state_tactic("unknown", mk_pair(0, 0));
+            return trace_state_tactic();
     });
 static register_tac reg_trace(name(g_tac, "trace"), [](type_checker & tc, expr const & e, pos_info_provider const *) {
         buffer<expr> args;

src/library/tactic/tactic.cpp

@@ -112,6 +112,14 @@ tactic trace_state_tactic(std::string const & fname, std::pair<unsigned, unsigne
         });
 }
 
+tactic trace_state_tactic() {
+    return tactic1([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state {
+            diagnostic(env, ios) << "proof state\n" << s << endl;
+            ios.get_diagnostic_channel().get_stream().flush();
+            return s;
+        });
+}
+
 tactic suppress_trace(tactic const & t) {
     return tactic([=](environment const & env, io_state const & ios, proof_state const & s) -> proof_state_seq {
             io_state new_ios(ios);

src/library/tactic/tactic.h

@@ -53,6 +53,7 @@ tactic trace_tactic(sstream const & msg);
 tactic trace_tactic(std::string const & msg);
 /** \brief Return a tactic that just displays the input state in the diagnostic channel. */
 tactic trace_state_tactic(std::string const & fname, std::pair<unsigned, unsigned> const & pos);
+tactic trace_state_tactic();
 /** \brief Create a tactic that applies \c t, but suppressing diagnostic messages. */
 tactic suppress_trace(tactic const & t);
 /** \brief Return a tactic that performs \c t1 followed by \c t2. */