From b8b6b219c3bc024eb241be39ca6cea2d4c85c503 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 28 Apr 2024 19:24:48 +0200 Subject: [PATCH] chore: move `trace.cpp` to kernel (#4014) Motivation: trace kernel `is_def_eq` --- src/kernel/CMakeLists.txt | 2 +- src/kernel/init_module.cpp | 3 +++ src/{library => kernel}/trace.cpp | 2 +- src/{library => kernel}/trace.h | 0 src/library/CMakeLists.txt | 2 +- src/library/compiler/borrowed_annotation.cpp | 2 +- src/library/compiler/compiler.cpp | 2 +- src/library/compiler/csimp.cpp | 2 +- src/library/compiler/eager_lambda_lifting.cpp | 2 +- src/library/compiler/extract_closed.cpp | 2 +- src/library/compiler/ir.cpp | 2 +- src/library/compiler/ir_interpreter.cpp | 2 +- src/library/compiler/lambda_lifting.cpp | 2 +- src/library/compiler/llnf.cpp | 2 +- src/library/compiler/specialize.cpp | 2 +- src/library/compiler/struct_cases_on.cpp | 2 +- src/library/compiler/util.cpp | 2 +- src/library/init_module.cpp | 3 --- src/library/time_task.cpp | 2 +- src/util/shell.cpp | 2 +- 20 files changed, 20 insertions(+), 20 deletions(-) rename src/{library => kernel}/trace.cpp (99%) rename src/{library => kernel}/trace.h (100%) diff --git a/src/kernel/CMakeLists.txt b/src/kernel/CMakeLists.txt index e611840a97..9b9c1e42d6 100644 --- a/src/kernel/CMakeLists.txt +++ b/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) diff --git a/src/kernel/init_module.cpp b/src/kernel/init_module.cpp index 3581567db2..d676c46faa 100644 --- a/src/kernel/init_module.cpp +++ b/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(); diff --git a/src/library/trace.cpp b/src/kernel/trace.cpp similarity index 99% rename from src/library/trace.cpp rename to src/kernel/trace.cpp index a20eca8c9a..9cec464e5f 100644 --- a/src/library/trace.cpp +++ b/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; diff --git a/src/library/trace.h b/src/kernel/trace.h similarity index 100% rename from src/library/trace.h rename to src/kernel/trace.h diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt index 961df78a77..cd0980097c 100644 --- a/src/library/CMakeLists.txt +++ b/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) diff --git a/src/library/compiler/borrowed_annotation.cpp b/src/library/compiler/borrowed_annotation.cpp index 0d215f8c91..ed3b2483dd 100644 --- a/src/library/compiler/borrowed_annotation.cpp +++ b/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" diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp index cf933ef8ec..eb75c93a27 100644 --- a/src/library/compiler/compiler.cpp +++ b/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" diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp index 34d5e51ade..3a15b38bfe 100644 --- a/src/library/compiler/csimp.cpp +++ b/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" diff --git a/src/library/compiler/eager_lambda_lifting.cpp b/src/library/compiler/eager_lambda_lifting.cpp index a1b260e5b2..2f838dad1f 100644 --- a/src/library/compiler/eager_lambda_lifting.cpp +++ b/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" diff --git a/src/library/compiler/extract_closed.cpp b/src/library/compiler/extract_closed.cpp index 2975c0f95d..929b49e6a3 100644 --- a/src/library/compiler/extract_closed.cpp +++ b/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" diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp index 66fe766585..55c333ea6d 100644 --- a/src/library/compiler/ir.cpp +++ b/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" diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp index a25a9c65ac..ce6698ac11 100644 --- a/src/library/compiler/ir_interpreter.cpp +++ b/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" diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp index 39b78104f4..176db6baae 100644 --- a/src/library/compiler/lambda_lifting.cpp +++ b/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" diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp index b2f55a8d78..0c8b453ce9 100644 --- a/src/library/compiler/llnf.cpp +++ b/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" diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp index c58012f5b8..e6aa59c715 100644 --- a/src/library/compiler/specialize.cpp +++ b/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" diff --git a/src/library/compiler/struct_cases_on.cpp b/src/library/compiler/struct_cases_on.cpp index 3e2613f569..50d26c8749 100644 --- a/src/library/compiler/struct_cases_on.cpp +++ b/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" diff --git a/src/library/compiler/util.cpp b/src/library/compiler/util.cpp index 789cfb0aac..2d9e742cd0 100644 --- a/src/library/compiler/util.cpp +++ b/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" diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp index d4678e5b54..4824c640ac 100644 --- a/src/library/init_module.cpp +++ b/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(); diff --git a/src/library/time_task.cpp b/src/library/time_task.cpp index 89c15061ba..8a1c2b3b62 100644 --- a/src/library/time_task.cpp +++ b/src/library/time_task.cpp @@ -7,7 +7,7 @@ Author: Sebastian Ullrich #include #include #include "library/time_task.h" -#include "library/trace.h" +#include "kernel/trace.h" namespace lean { diff --git a/src/util/shell.cpp b/src/util/shell.cpp index 1209672b4a..7ac5ec0574 100644 --- a/src/util/shell.cpp +++ b/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"