diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index b00049c2ba..e9dba6ac24 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -402,16 +402,10 @@ else()
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:kernel>)
   add_subdirectory(library)
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:library>)
-  add_subdirectory(library/tactic)
-  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:tactic>)
   add_subdirectory(library/constructions)
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:constructions>)
-  add_subdirectory(library/equations_compiler)
-  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:equations_compiler>)
   add_subdirectory(library/compiler)
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:compiler>)
-  add_subdirectory(frontends/lean)
-  set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:lean_frontend>)
   add_subdirectory(initialize)
   set(LEAN_OBJS ${LEAN_OBJS} $<TARGET_OBJECTS:initialize>)
   if(${STAGE} EQUAL 0)
diff --git a/src/initialize/init.cpp b/src/initialize/init.cpp
index 07f1fd535e..6d19e8b9ae 100644
--- a/src/initialize/init.cpp
+++ b/src/initialize/init.cpp
@@ -11,12 +11,9 @@ Author: Leonardo de Moura
 #include "util/io.h"
 #include "kernel/init_module.h"
 #include "library/init_module.h"
-#include "library/tactic/init_module.h"
 #include "library/constructions/init_module.h"
-#include "library/equations_compiler/init_module.h"
 #include "library/print.h"
 #include "library/compiler/init_module.h"
-#include "frontends/lean/init_module.h"
 #include "initialize/init.h"
 
 namespace lean {
@@ -33,10 +30,7 @@ extern "C" void lean_initialize() {
     initialize_library_core_module();
     initialize_library_module();
     initialize_compiler_module();
-    initialize_tactic_module();
     initialize_constructions_module();
-    initialize_equations_compiler_module();
-    initialize_frontend_lean_module();
 }
 
 void initialize() {
@@ -45,10 +39,7 @@ void initialize() {
 
 void finalize() {
     run_thread_finalizers();
-    finalize_frontend_lean_module();
-    finalize_equations_compiler_module();
     finalize_constructions_module();
-    finalize_tactic_module();
     finalize_compiler_module();
     finalize_library_module();
     finalize_library_core_module();
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index ba82aeeaf2..0c19f64a12 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -383,10 +383,23 @@ void environment_free_regions(environment && env) {
     consume_io_result(lean_environment_free_regions(env.steal(), io_mk_world()));
 }
 
-pos_info get_message_pos(object_ref const & msg);
-message_severity get_message_severity(object_ref const & msg);
-std::string get_message_string(object_ref const & msg);
+extern "C" object * lean_message_pos(object * msg);
+extern "C" uint8 lean_message_severity(object * msg);
+extern "C" object * lean_message_string(object * msg);
 
+pos_info get_message_pos(object_ref const & msg) {
+    auto p = pair_ref<nat, nat>(lean_message_pos(msg.to_obj_arg()));
+    return pos_info(p.fst().get_small_value(), p.snd().get_small_value());
+}
+
+message_severity get_message_severity(object_ref const & msg) {
+    return static_cast<message_severity>(lean_message_severity(msg.to_obj_arg()));
+}
+
+std::string get_message_string(object_ref const & msg) {
+    string_ref r(lean_message_string(msg.to_obj_arg()));
+    return r.to_std_string();
+}
 }
 
 void check_optarg(char const * option_name) {