chore: move the IR interpreter from library/compiler to library (#9265)

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)

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)

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 &):

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"

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();

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();

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"
 

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