From d664486ecafc8e356f8769afe108943ca1012a1a Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 7 Jun 2019 10:58:23 -0700 Subject: [PATCH] chore(util): move format to `src/util` --- src/CMakeLists.txt | 3 ++- src/frontends/lean/pp.h | 2 +- src/kernel/expr.h | 2 +- src/kernel/level.h | 2 +- src/library/formatter.h | 2 +- src/library/pos_info_provider.h | 2 +- src/util/CMakeLists.txt | 2 +- src/util/{sexpr => }/format.cpp | 5 +---- src/util/{sexpr => }/format.h | 0 src/util/init_module.cpp | 3 +++ src/util/sexpr/CMakeLists.txt | 2 +- src/util/sexpr/init_module.cpp | 3 --- 12 files changed, 13 insertions(+), 15 deletions(-) rename src/util/{sexpr => }/format.cpp (96%) rename src/util/{sexpr => }/format.h (100%) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 75c3541b54..67d9e0505c 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -501,7 +501,8 @@ function(add_exec_test name tgt) endif() endfunction() -add_subdirectory(tests/util) +# C++ unit tests are disabled for now since they rely on `format` which relies on `Lean` generated code. +# add_subdirectory(tests/util) # Include style check if (NOT(${CMAKE_SYSTEM_NAME} MATCHES "Windows") AND PYTHONINTERP_FOUND) diff --git a/src/frontends/lean/pp.h b/src/frontends/lean/pp.h index 4e08f8095a..5e1bd53582 100644 --- a/src/frontends/lean/pp.h +++ b/src/frontends/lean/pp.h @@ -13,7 +13,7 @@ Author: Leonardo de Moura #include "util/name_map.h" #include "util/name_set.h" #include "util/options.h" -#include "util/sexpr/format.h" +#include "util/format.h" #include "kernel/environment.h" #include "library/abstract_type_context.h" #include "frontends/lean/token_table.h" diff --git a/src/kernel/expr.h b/src/kernel/expr.h index 7b8f1c495d..fb6ebeb811 100644 --- a/src/kernel/expr.h +++ b/src/kernel/expr.h @@ -20,7 +20,7 @@ Author: Leonardo de Moura #include "util/buffer.h" #include "util/kvmap.h" #include "util/list_fn.h" -#include "util/sexpr/format.h" +#include "util/format.h" #include "kernel/level.h" #include "kernel/expr_eq_fn.h" diff --git a/src/kernel/level.h b/src/kernel/level.h index 3201083162..8ef4fbfa64 100644 --- a/src/kernel/level.h +++ b/src/kernel/level.h @@ -12,7 +12,7 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/list_ref.h" #include "util/options.h" -#include "util/sexpr/format.h" +#include "util/format.h" namespace lean { class environment; diff --git a/src/library/formatter.h b/src/library/formatter.h index 4c7bfab2f1..281df56931 100644 --- a/src/library/formatter.h +++ b/src/library/formatter.h @@ -8,7 +8,7 @@ Author: Leonardo de Moura #include #include #include "util/options.h" -#include "util/sexpr/format.h" +#include "util/format.h" namespace lean { class expr; diff --git a/src/library/pos_info_provider.h b/src/library/pos_info_provider.h index 9367108dfe..161a7e1ee1 100644 --- a/src/library/pos_info_provider.h +++ b/src/library/pos_info_provider.h @@ -6,7 +6,7 @@ Author: Leonardo de Moura */ #pragma once #include -#include "util/sexpr/format.h" +#include "util/format.h" #include "kernel/expr.h" #include "util/message_definitions.h" diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 7f269558b8..742bcb2b86 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -3,4 +3,4 @@ add_library(util OBJECT object_ref.cpp name.cpp name_set.cpp fresh_name.cpp path.cpp lean_path.cpp lbool.cpp bitap_fuzzy_search.cpp init_module.cpp list_fn.cpp file_lock.cpp timeit.cpp timer.cpp parser_exception.cpp name_generator.cpp kvmap.cpp map_foreach.cpp - options.cpp option_declarations.cpp) + options.cpp format.cpp option_declarations.cpp) diff --git a/src/util/sexpr/format.cpp b/src/util/format.cpp similarity index 96% rename from src/util/sexpr/format.cpp rename to src/util/format.cpp index 6e8cac5d16..d826c93e4d 100644 --- a/src/util/sexpr/format.cpp +++ b/src/util/format.cpp @@ -13,12 +13,9 @@ #include "runtime/interrupt.h" #include "runtime/sstream.h" #include "runtime/hash.h" -#include "util/escaped.h" -#include "util/sexpr/sexpr.h" -#include "util/sexpr/format.h" -#include "util/sexpr/sexpr_fn.h" #include "util/options.h" #include "util/option_declarations.h" +#include "util/format.h" #ifndef LEAN_DEFAULT_PP_INDENTATION #define LEAN_DEFAULT_PP_INDENTATION 2 diff --git a/src/util/sexpr/format.h b/src/util/format.h similarity index 100% rename from src/util/sexpr/format.h rename to src/util/format.h diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp index c01f139537..a65e02ded5 100644 --- a/src/util/init_module.cpp +++ b/src/util/init_module.cpp @@ -11,6 +11,7 @@ Author: Leonardo de Moura #include "util/name_generator.h" #include "util/options.h" #include "util/option_declarations.h" +#include "util/format.h" namespace lean { void initialize_util_module() { @@ -21,8 +22,10 @@ void initialize_util_module() { initialize_fresh_name(); initialize_option_declarations(); initialize_options(); + initialize_format(); } void finalize_util_module() { + finalize_format(); finalize_options(); finalize_option_declarations(); finalize_fresh_name(); diff --git a/src/util/sexpr/CMakeLists.txt b/src/util/sexpr/CMakeLists.txt index f98364172e..d09a472ec9 100644 --- a/src/util/sexpr/CMakeLists.txt +++ b/src/util/sexpr/CMakeLists.txt @@ -1 +1 @@ -add_library(sexpr OBJECT sexpr.cpp sexpr_fn.cpp format.cpp init_module.cpp) +add_library(sexpr OBJECT sexpr.cpp sexpr_fn.cpp init_module.cpp) diff --git a/src/util/sexpr/init_module.cpp b/src/util/sexpr/init_module.cpp index 48f7272dd8..2ef7fd20b1 100644 --- a/src/util/sexpr/init_module.cpp +++ b/src/util/sexpr/init_module.cpp @@ -4,17 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include "util/sexpr/format.h" #include "util/sexpr/sexpr.h" namespace lean { void initialize_sexpr_module() { initialize_sexpr(); - initialize_format(); } void finalize_sexpr_module() { - finalize_format(); finalize_sexpr(); } }