diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 2bd6cca20a..a261c93f69 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -7,4 +7,6 @@ add_library(library OBJECT expr_lt.cpp
   aux_recursors.cpp
   profiling.cpp time_task.cpp
   formatter.cpp
-  elab_environment.cpp)
+  elab_environment.cpp
+  init_attribute.cpp
+  ir_interpreter.cpp)
diff --git a/src/library/compiler/CMakeLists.txt b/src/library/compiler/CMakeLists.txt
index fef4649a2d..96d71de0e7 100644
--- a/src/library/compiler/CMakeLists.txt
+++ b/src/library/compiler/CMakeLists.txt
@@ -4,6 +4,6 @@ add_library(compiler OBJECT init_module.cpp ## New
   extract_closed.cpp simp_app_args.cpp llnf.cpp ll_infer_type.cpp
   reduce_arity.cpp closed_term_cache.cpp
   export_attribute.cpp extern_attribute.cpp
-  borrowed_annotation.cpp init_attribute.cpp eager_lambda_lifting.cpp
+  borrowed_annotation.cpp eager_lambda_lifting.cpp
   struct_cases_on.cpp find_jp.cpp ir.cpp implemented_by_attribute.cpp
-  ir_interpreter.cpp llvm.cpp noncomputable_attribute.cpp)
+  llvm.cpp noncomputable_attribute.cpp)
diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 1bc325dac8..b4722de231 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -26,7 +26,7 @@ Author: Leonardo de Moura
 #include "library/compiler/csimp.h"
 #include "library/compiler/extract_closed.h"
 #include "library/compiler/reduce_arity.h"
-#include "library/compiler/init_attribute.h"
+#include "library/init_attribute.h"
 
 namespace lean {
 csimp_cfg::csimp_cfg(options const &):
diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp
index 5c00d3a89f..e6ab5b1a6d 100644
--- a/src/library/compiler/extern_attribute.cpp
+++ b/src/library/compiler/extern_attribute.cpp
@@ -14,7 +14,7 @@ Authors: Leonardo de Moura
 #include "library/util.h"
 #include "library/projection.h"
 #include "library/compiler/borrowed_annotation.h"
-#include "library/compiler/init_attribute.h"
+#include "library/init_attribute.h"
 #include "library/compiler/implemented_by_attribute.h"
 #include "library/compiler/util.h"
 #include "library/compiler/ir.h"
diff --git a/src/library/compiler/init_module.cpp b/src/library/compiler/init_module.cpp
index 851a90f611..2dde8d92bb 100644
--- a/src/library/compiler/init_module.cpp
+++ b/src/library/compiler/init_module.cpp
@@ -15,7 +15,6 @@ Author: Leonardo de Moura
 #include "library/compiler/borrowed_annotation.h"
 #include "library/compiler/ll_infer_type.h"
 #include "library/compiler/ir.h"
-#include "library/compiler/ir_interpreter.h"
 
 namespace lean {
 void initialize_compiler_module() {
@@ -29,11 +28,9 @@ void initialize_compiler_module() {
     initialize_borrowed_annotation();
     initialize_ll_infer_type();
     initialize_ir();
-    initialize_ir_interpreter();
 }
 
 void finalize_compiler_module() {
-    finalize_ir_interpreter();
     finalize_ir();
     finalize_ll_infer_type();
     finalize_borrowed_annotation();
diff --git a/src/library/compiler/init_attribute.cpp b/src/library/init_attribute.cpp
similarity index 100%
rename from src/library/compiler/init_attribute.cpp
rename to src/library/init_attribute.cpp
diff --git a/src/library/compiler/init_attribute.h b/src/library/init_attribute.h
similarity index 100%
rename from src/library/compiler/init_attribute.h
rename to src/library/init_attribute.h
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 14a26103b1..1251a7cd28 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "library/time_task.h"
 #include "library/formatter.h"
 #include "library/dynlib.h"
+#include "library/ir_interpreter.h"
 
 namespace lean {
 void initialize_library_core_module() {
@@ -37,9 +38,11 @@ void initialize_library_module() {
     initialize_library_util();
     initialize_time_task();
     initialize_dynlib();
+    initialize_ir_interpreter();
 }
 
 void finalize_library_module() {
+    finalize_ir_interpreter();
     finalize_time_task();
     finalize_library_util();
     finalize_class();
diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/ir_interpreter.cpp
similarity index 99%
rename from src/library/compiler/ir_interpreter.cpp
rename to src/library/ir_interpreter.cpp
index 7f7c5b5232..d8ce7da81b 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/ir_interpreter.cpp
@@ -35,7 +35,7 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #else
 #include <dlfcn.h>
 #endif
-#include "library/compiler/ir_interpreter.h"
+#include "library/ir_interpreter.h"
 #include "runtime/flet.h"
 #include "runtime/apply.h"
 #include "runtime/interrupt.h"
@@ -46,7 +46,7 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #include "library/constants.h"
 #include "library/time_task.h"
 #include "library/ir_types.h"
-#include "library/compiler/init_attribute.h"
+#include "library/init_attribute.h"
 #include "util/nat.h"
 #include "util/option_declarations.h"
 
diff --git a/src/library/compiler/ir_interpreter.h b/src/library/ir_interpreter.h
similarity index 100%
rename from src/library/compiler/ir_interpreter.h
rename to src/library/ir_interpreter.h
diff --git a/src/util/shell.cpp b/src/util/shell.cpp
index f0789898fe..0f18cde0e2 100644
--- a/src/util/shell.cpp
+++ b/src/util/shell.cpp
@@ -38,7 +38,7 @@ Author: Leonardo de Moura
 #include "library/compiler/ir.h"
 #include "library/print.h"
 #include "initialize/init.h"
-#include "library/compiler/ir_interpreter.h"
+#include "library/ir_interpreter.h"
 #include "util/path.h"
 #include "stdlib_flags.h"
 #ifdef _MSC_VER