fix(library/tactic/tactic_state): remove problematic get_tactic_vm_state

src/frontends/smt2/parser.cpp

@@ -481,6 +481,7 @@ private:
         vm_obj s = to_obj(tactic_state(env(), ios().get_options(), mctx, list<expr>(goal_mvar), goal_mvar));
 
         vm_state state(env());
+        scope_vm_state scope(state);
         vm_obj result = state.invoke(get_smt_prove_name(), s);
         if (optional<tactic_state> s_new = is_tactic_success(result)) {
             mctx = s_new->mctx();

src/library/tactic/simplifier/simplifier.cpp

@@ -333,7 +333,7 @@ class simplifier {
             expr goal_type = mk_app(m_tctx, m_rel, old_e, result_mvar);
             expr goal_mvar = mctx.mk_metavar_decl(m_tctx.lctx(), goal_type);
             vm_obj s = to_obj(tactic_state(m_tctx.env(), m_tctx.get_options(), mctx, list<expr>(goal_mvar), goal_mvar));
-            vm_obj simp_ext_result = get_tactic_vm_state(m_tctx.env()).invoke(ext_id, 1, &s);
+            vm_obj simp_ext_result = invoke(ext_id, s);
             optional<tactic_state> s_new = is_tactic_success(simp_ext_result);
             // TODO(dhs): create a bool metavar for the `done` flag
             if (s_new) {

src/library/tactic/tactic_state.cpp

@@ -495,13 +495,6 @@ vm_obj tactic_is_trace_enabled_for(vm_obj const & n) {
     return mk_vm_bool(is_trace_class_enabled(to_name(n)));
 }
 
-typedef transparencyless_cache_compatibility_helper<vm_state> vm_state_cache_helper;
-MK_THREAD_LOCAL_GET_DEF(vm_state_cache_helper, get_vmsc);
-
-vm_state & get_tactic_vm_state(environment const & env) {
-    return get_vmsc().get_cache_for(env);
-}
-
 vm_obj tactic_instantiate_mvars(vm_obj const & e, vm_obj const & _s) {
     tactic_state const & s = to_tactic_state(_s);
     metavar_context mctx = s.mctx();

src/library/tactic/tactic_state.h

@@ -147,8 +147,6 @@ inline type_context mk_type_context_for(vm_obj const & s, vm_obj const & m) {
 #define LEAN_TACTIC_TRY try {
 #define LEAN_TACTIC_CATCH(S) } catch (exception const & ex) { return mk_tactic_exception(ex, S); }
 
-vm_state & get_tactic_vm_state(environment const & env);
-
 void initialize_tactic_state();
 void finalize_tactic_state();
 }

src/library/vm/vm.cpp

@@ -1646,6 +1646,16 @@ vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args) {
     return g_vm_state->invoke(fn, nargs, args);
 }
 
+vm_obj invoke(unsigned fn_idx, unsigned nargs, vm_obj const * args) {
+    lean_assert(g_vm_state);
+    vm_obj fn = mk_vm_closure(fn_idx, 0, nullptr);
+    return invoke(fn, nargs, args);
+}
+
+vm_obj invoke(unsigned fn_idx, vm_obj const & arg) {
+    return invoke(fn_idx, 1, &arg);
+}
+
 vm_state const & get_vm_state() {
     lean_assert(g_vm_state);
     return *g_vm_state;

src/library/vm/vm.h

@@ -693,6 +693,9 @@ vm_obj invoke(vm_obj const & fn, vm_obj const & a1, vm_obj const & a2, vm_obj co
               vm_obj const & a5, vm_obj const & a6, vm_obj const & a7, vm_obj const & a8);
 vm_obj invoke(vm_obj const & fn, unsigned nargs, vm_obj const * args);
 
+vm_obj invoke(unsigned fn_idx, unsigned nargs, vm_obj const * args);
+vm_obj invoke(unsigned fn_idx, vm_obj const & arg);
+
 void display_vm_code(std::ostream & out, environment const & env, unsigned code_sz, vm_instr const * code);
 
 void initialize_vm_core();