chore: move trace.cpp to kernel (#4014)

Motivation: trace kernel `is_def_eq`

src/kernel/CMakeLists.txt

@@ -2,4 +2,4 @@ add_library(kernel OBJECT level.cpp expr.cpp expr_eq_fn.cpp
 for_each_fn.cpp replace_fn.cpp abstract.cpp instantiate.cpp
 local_ctx.cpp declaration.cpp environment.cpp type_checker.cpp
 init_module.cpp expr_cache.cpp equiv_manager.cpp quot.cpp
-inductive.cpp)
+inductive.cpp trace.cpp)

src/kernel/init_module.cpp

@@ -12,6 +12,7 @@ Author: Leonardo de Moura
 #include "kernel/local_ctx.h"
 #include "kernel/inductive.h"
 #include "kernel/quot.h"
+#include "kernel/trace.h"
 
 namespace lean {
 void initialize_kernel_module() {
@@ -23,9 +24,11 @@ void initialize_kernel_module() {
     initialize_local_ctx();
     initialize_inductive();
     initialize_quot();
+    initialize_trace();
 }
 
 void finalize_kernel_module() {
+    finalize_trace();
     finalize_quot();
     finalize_inductive();
     finalize_local_ctx();

src/kernel/trace.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "util/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/local_ctx.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 
 namespace lean {
 static name_set *            g_trace_classes = nullptr;

src/library/CMakeLists.txt

@@ -4,6 +4,6 @@ add_library(library OBJECT expr_lt.cpp
   class.cpp util.cpp print.cpp annotation.cpp
   protected.cpp reducible.cpp init_module.cpp
   projection.cpp
-  aux_recursors.cpp trace.cpp
+  aux_recursors.cpp
   profiling.cpp time_task.cpp
   formatter.cpp)

src/library/compiler/borrowed_annotation.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/instantiate.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 #include "library/annotation.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"

src/library/compiler/compiler.cpp

@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include "util/io.h"
 #include "kernel/type_checker.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/trace.h"
 #include "library/max_sharing.h"
-#include "library/trace.h"
 #include "library/time_task.h"
 #include "library/compiler/util.h"
 #include "library/compiler/lcnf.h"

src/library/compiler/csimp.cpp

@@ -15,10 +15,10 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/inductive.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/trace.h"
 #include "library/util.h"
 #include "library/constants.h"
 #include "library/class.h"
-#include "library/trace.h"
 #include "library/expr_pair_maps.h"
 #include "library/compiler/util.h"
 #include "library/compiler/cse.h"

src/library/compiler/eager_lambda_lifting.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/type_checker.h"
 #include "kernel/inductive.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 #include "library/class.h"
 #include "library/compiler/util.h"
 #include "library/compiler/csimp.h"

src/library/compiler/extract_closed.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/expr_maps.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/inductive.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/closed_term_cache.h"
 #include "library/compiler/reduce_arity.h"

src/library/compiler/ir.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "util/nat.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"
 #include "library/compiler/extern_attribute.h"

src/library/compiler/ir_interpreter.cpp

@@ -40,8 +40,8 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #include "runtime/io.h"
 #include "runtime/option_ref.h"
 #include "runtime/array_ref.h"
+#include "kernel/trace.h"
 #include "library/time_task.h"
-#include "library/trace.h"
 #include "library/compiler/ir.h"
 #include "library/compiler/init_attribute.h"
 #include "util/nat.h"

src/library/compiler/lambda_lifting.cpp

@@ -10,7 +10,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/inductive.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/closed_term_cache.h"
 

src/library/compiler/llnf.cpp

@@ -16,8 +16,8 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/inductive.h"
+#include "kernel/trace.h"
 #include "library/util.h"
-#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"
 #include "library/compiler/ll_infer_type.h"

src/library/compiler/specialize.cpp

@@ -10,8 +10,8 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/inductive.h"
+#include "kernel/trace.h"
 #include "library/class.h"
-#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/csimp.h"
 

src/library/compiler/struct_cases_on.cpp

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
 #include "kernel/inductive.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 #include "library/suffixes.h"
 #include "library/compiler/util.h"
 

src/library/compiler/util.cpp

@@ -18,12 +18,12 @@ Author: Leonardo de Moura
 #include "kernel/inductive.h"
 #include "kernel/instantiate.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/trace.h"
 #include "library/util.h"
 #include "library/suffixes.h"
 #include "library/aux_recursors.h"
 #include "library/replace_visitor.h"
 #include "library/constants.h"
-#include "library/trace.h"
 #include "library/compiler/lambda_lifting.h"
 #include "library/compiler/eager_lambda_lifting.h"
 #include "library/compiler/util.h"

src/library/init_module.cpp

@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include "library/trace.h"
 #include "library/constants.h"
 #include "library/class.h"
 #include "library/num.h"
@@ -21,11 +20,9 @@ void initialize_library_core_module() {
     initialize_formatter();
     initialize_constants();
     initialize_profiling();
-    initialize_trace();
 }
 
 void finalize_library_core_module() {
-    finalize_trace();
     finalize_profiling();
     finalize_constants();
     finalize_formatter();

src/library/time_task.cpp

@@ -7,7 +7,7 @@ Author: Sebastian Ullrich
 #include <string>
 #include <map>
 #include "library/time_task.h"
-#include "library/trace.h"
+#include "kernel/trace.h"
 
 namespace lean {
 

src/util/shell.cpp

@@ -29,11 +29,11 @@ Author: Leonardo de Moura
 #include "util/option_declarations.h"
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/trace.h"
 #include "library/formatter.h"
 #include "library/module.h"
 #include "library/time_task.h"
 #include "library/compiler/ir.h"
-#include "library/trace.h"
 #include "library/print.h"
 #include "initialize/init.h"
 #include "library/compiler/ir_interpreter.h"