fix(library/tactic/smt): add temporary hack to workaround revert-all issue

src/library/local_context.h

@@ -118,6 +118,9 @@ class local_context {
       - If `freeze_local_instances` is not set, then type_context will compute
         local instances during initialization. This is needed to be able to elaborate
         parameter.
+
+       The solution above is incompatible with the `revert-all, do something, reintroduce`
+       idiom. This idiom is used to implement `dsimp *` and SMT tactic.
     */
     optional<unsigned>     m_instance_fingerprint;
     friend class type_context;
@@ -144,6 +147,12 @@ public:
         return lctx;
     }
 
+    /* Temporary hack to make sure we can use SMT tactic until we fix the m_instance_fingerprint issue
+       described above. */
+    void reset_instance_fingerprint() {
+        m_instance_fingerprint = optional<unsigned>();
+    }
+
     optional<unsigned> get_instance_fingerprint() const { return m_instance_fingerprint; }
 
     bool empty() const { return m_idx2local_decl.empty(); }

src/library/tactic/revert_tactic.cpp

@@ -27,6 +27,19 @@ tactic_state revert(buffer<expr> & locals, tactic_state const & s, bool preserve
     return set_mctx_goals(s, mctx, cons(new_g, tail(s.goals())));
 }
 
+/* Temporary hack to make sure we can use SMT tactics until we fix the m_instance_fingerprint issue */
+tactic_state reset_instance_fingerprint(tactic_state const & s) {
+    lean_assert(s.goals());
+    metavar_context mctx = s.mctx();
+    expr mvar                  = head(s.goals());
+    optional<metavar_decl> g   = mctx.find_metavar_decl(mvar);
+    local_context lctx         = g->get_context();
+    lctx.reset_instance_fingerprint();
+    expr new_mvar              = mctx.mk_metavar_decl(lctx, g->get_type());
+    mctx.assign(mvar, new_mvar);
+    return set_mctx_goals(s, mctx, cons(new_mvar, tail(s.goals())));
+}
+
 vm_obj revert(list<expr> const & ls, tactic_state const & s, bool preserve_locals_order) {
     optional<metavar_decl> g   = s.get_main_goal_decl();
     if (!g) return mk_no_goals_exception(s);

src/library/tactic/revert_tactic.h

@@ -16,6 +16,9 @@ tactic_state revert(buffer<expr> & hs, tactic_state const & s, bool preserve_hs_
 expr revert(environment const & env, options const & opts, metavar_context & mctx, expr const & mvar, buffer<expr> & locals,
             bool preserve_locals_order);
 
+// temp hack
+tactic_state reset_instance_fingerprint(tactic_state const & s);
+
 void initialize_revert_tactic();
 void finalize_revert_tactic();
 }

src/library/tactic/smt/smt_state.cpp

@@ -400,8 +400,9 @@ tactic_state add_em_facts(tactic_state const & ts, smt_goal & g) {
 vm_obj mk_smt_state(tactic_state s, smt_config const & cfg) {
     if (!s.goals()) return mk_no_goals_exception(s);
     unsigned num_reverted;
+    /* TODO(Leo): revert-all is an anti-idiom. See discussion at m_instance_fingerprint. */
     std::tie(s, num_reverted) = revert_all(clear_recs(s));
-
+    s = reset_instance_fingerprint(s);
     smt_goal new_goal(cfg);
 
     vm_obj r = preprocess(s, cfg.m_pre_config);