From d40e97b4bcf0e85e9aa60722f4686beed78de1e7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 29 Nov 2016 11:29:07 -0800 Subject: [PATCH] chore(*): compilation errors, fix style, fix warnings --- src/api/parser.cpp | 4 +--- src/frontends/lean/info_manager.cpp | 2 +- src/frontends/lean/info_manager.h | 2 +- src/frontends/lean/parser.cpp | 31 +++++++++++++++++++---------- src/frontends/lean/parser.h | 7 +++---- src/kernel/declaration.cpp | 3 ++- src/library/export_decl.h | 1 + src/library/message_builder.cpp | 2 +- src/library/module.h | 2 +- src/library/module_mgr.cpp | 12 +++++------ src/library/module_mgr.h | 8 ++++---- src/library/mt_task_queue.h | 2 +- src/library/versioned_msg_buf.cpp | 2 +- src/library/versioned_msg_buf.h | 2 +- src/shell/lean.cpp | 6 +++--- src/shell/server.cpp | 18 ++++++++--------- src/shell/server.h | 4 ++-- src/util/interrupt.cpp | 2 +- src/util/interrupt.h | 3 +-- 19 files changed, 60 insertions(+), 53 deletions(-) diff --git a/src/api/parser.cpp b/src/api/parser.cpp index 7cdd48ba48..341f05af6f 100644 --- a/src/api/parser.cpp +++ b/src/api/parser.cpp @@ -20,9 +20,7 @@ lean_bool lean_parse_file(lean_env env, lean_ios ios, char const * fname, lean_e check_nonnull(fname); environment _env = to_env_ref(env); io_state _ios = to_io_state_ref(ios); - bool use_exceptions = true; - unsigned num_threads = 1; - parse_commands(_env, _ios, fname, optional(), use_exceptions, num_threads); + parse_commands(_env, _ios, fname); *new_env = of_env(new environment(_env)); *new_ios = of_io_state(new io_state(_ios)); LEAN_CATCH; diff --git a/src/frontends/lean/info_manager.cpp b/src/frontends/lean/info_manager.cpp index ba41087d36..df2a283dc8 100644 --- a/src/frontends/lean/info_manager.cpp +++ b/src/frontends/lean/info_manager.cpp @@ -8,12 +8,12 @@ Author: Leonardo de Moura #include #include #include -#include "frontends/lean/info_manager.h" #include "util/lean_path.h" #include "library/choice.h" #include "library/scoped_ext.h" #include "library/pp_options.h" #include "frontends/lean/json.h" +#include "frontends/lean/info_manager.h" namespace lean { class type_info_data : public info_data_cell { diff --git a/src/frontends/lean/info_manager.h b/src/frontends/lean/info_manager.h index cb9eb45715..88fba466dc 100644 --- a/src/frontends/lean/info_manager.h +++ b/src/frontends/lean/info_manager.h @@ -10,9 +10,9 @@ Author: Leonardo de Moura #include #include "kernel/expr.h" #include "library/io_state_stream.h" -#include "frontends/lean/json.h" #include "library/metavar_context.h" #include "library/tactic/tactic_state.h" +#include "frontends/lean/json.h" namespace lean { diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp index a75edb4347..638b3e49ce 100644 --- a/src/frontends/lean/parser.cpp +++ b/src/frontends/lean/parser.cpp @@ -9,9 +9,6 @@ Author: Leonardo de Moura #include #include #include "util/utf8.h" -#include -#include "library/st_task_queue.h" -#include "library/module_mgr.h" #include "util/interrupt.h" #include "util/sstream.h" #include "util/flet.h" @@ -23,6 +20,8 @@ Author: Leonardo de Moura #include "kernel/abstract.h" #include "kernel/instantiate.h" #include "kernel/error_msgs.h" +#include "library/st_task_queue.h" +#include "library/module_mgr.h" #include "library/export_decl.h" #include "library/trace.h" #include "library/exception.h" @@ -2054,6 +2053,10 @@ void parser::reset_doc_string() { m_doc_string = optional(); } +#if defined(__GNUC__) && !defined(__CLANG__) +#pragma GCC diagnostic ignored "-Wmaybe-uninitialized" +#endif + std::vector parser::parse_imports(unsigned & fingerprint) { m_last_cmd_pos = pos(); bool prelude = false; @@ -2070,19 +2073,25 @@ std::vector parser::parse_imports(unsigned & fingerprint) { next(); while (true) { optional k; + unsigned h = 0; while (true) { if (curr_is_token(get_period_tk())) { next(); - if (!k) + if (!k) { k = 0; - else + } else { k = *k + 1; + h++; + } } else if (curr_is_token(get_ellipsis_tk())) { next(); - if (!k) + if (!k) { k = 2; - else + h = 2; + } else { k = *k + 3; + h += 3; + } } else { break; } @@ -2091,8 +2100,9 @@ std::vector parser::parse_imports(unsigned & fingerprint) { break; name f = get_name_val(); fingerprint = hash(fingerprint, f.hash()); - if (k) - fingerprint = hash(fingerprint, *k); + if (k) { + fingerprint = hash(fingerprint, h); + } imports.push_back({ f, k }); next(); } @@ -2262,8 +2272,7 @@ message_builder parser::mk_message(message_severity severity) { return mk_message(pos(), severity); } -bool parse_commands(environment & env, io_state & ios, char const * fname, optional const & base_dir, - bool use_exceptions, unsigned num_threads) { +bool parse_commands(environment & env, io_state & ios, char const * fname) { st_task_queue tq; scope_global_task_queue scope(&tq); fs_module_vfs vfs; diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h index 15bcc30679..ee2a59afe0 100644 --- a/src/frontends/lean/parser.h +++ b/src/frontends/lean/parser.h @@ -8,13 +8,13 @@ Author: Leonardo de Moura #include #include #include -#include "library/module.h" #include "util/flet.h" #include "util/name_map.h" #include "util/exception.h" -#include "library/task_queue.h" #include "kernel/environment.h" #include "kernel/expr_maps.h" +#include "library/module.h" +#include "library/task_queue.h" #include "library/abstract_parser.h" #include "library/io_state.h" #include "library/io_state_stream.h" @@ -502,8 +502,7 @@ public: virtual char const * get_file_name() const override; }; -bool parse_commands(environment & env, io_state & ios, char const * fname, optional const & base, - bool use_exceptions, unsigned num_threads); +bool parse_commands(environment & env, io_state & ios, char const * fname); void initialize_parser(); void finalize_parser(); diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp index 4e97e9c046..329ead377e 100644 --- a/src/kernel/declaration.cpp +++ b/src/kernel/declaration.cpp @@ -4,10 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ -#include #include "kernel/declaration.h" #include "kernel/environment.h" #include "kernel/for_each_fn.h" +// TODO(gebner, leo): kernel should not depend on library folder +#include "library/task_queue.h" namespace lean { int compare(reducibility_hints const & h1, reducibility_hints const & h2) { diff --git a/src/library/export_decl.h b/src/library/export_decl.h index 4e244ef7dc..52617d6a34 100644 --- a/src/library/export_decl.h +++ b/src/library/export_decl.h @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Leonardo de Moura */ +#pragma once #include "kernel/environment.h" namespace lean { diff --git a/src/library/message_builder.cpp b/src/library/message_builder.cpp index 1cc153912d..cf0a46406e 100644 --- a/src/library/message_builder.cpp +++ b/src/library/message_builder.cpp @@ -4,10 +4,10 @@ Released under Apache 2.0 license as described in the file LICENSE. Author: Gabriel Ebner */ +#include #include "library/message_builder.h" #include "library/type_context.h" #include "library/message_buffer.h" -#include namespace lean { diff --git a/src/library/module.h b/src/library/module.h index 133bdb98a6..efec7c7f18 100644 --- a/src/library/module.h +++ b/src/library/module.h @@ -11,10 +11,10 @@ Author: Leonardo de Moura #include #include "util/serializer.h" #include "util/optional.h" +#include "kernel/pos_info_provider.h" #include "kernel/inductive/inductive.h" #include "library/io_state.h" #include "library/task_queue.h" -#include "kernel/pos_info_provider.h" namespace lean { class corrupted_file_exception : public exception { diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp index 01c6d5deba..24878709b5 100644 --- a/src/library/module_mgr.cpp +++ b/src/library/module_mgr.cpp @@ -8,14 +8,14 @@ Author: Gabriel Ebner #include #include #include -#include "library/module_mgr.h" +#include #include "util/lean_path.h" -#include "frontends/lean/parser.h" +#include "util/file_lock.h" +#include "library/module_mgr.h" #include "library/module.h" #include "library/versioned_msg_buf.h" -#include -#include -#include +#include "frontends/lean/pp.h" +#include "frontends/lean/parser.h" namespace lean { @@ -309,7 +309,7 @@ snapshot_vector module_mgr::get_snapshots(module_id const & id) { } bool -module_mgr::get_snapshots_or_unchanged_module(module_id const &id, std::string const &contents, time_t mtime, +module_mgr::get_snapshots_or_unchanged_module(module_id const &id, std::string const &contents, time_t /* mtime */, snapshot_vector &vector) { if (!m_modules.count(id)) return false; diff --git a/src/library/module_mgr.h b/src/library/module_mgr.h index 8fcdbd1eeb..56bbfa0913 100644 --- a/src/library/module_mgr.h +++ b/src/library/module_mgr.h @@ -8,14 +8,14 @@ Author: Gabriel Ebner #include #include #include -#include -#include -#include #include -#include "frontends/lean/parser.h" +#include "util/name.h" +#include "kernel/environment.h" +#include "library/task_queue.h" #include "library/message_buffer.h" #include "library/io_state.h" #include "library/trace.h" +#include "frontends/lean/parser.h" namespace lean { diff --git a/src/library/mt_task_queue.h b/src/library/mt_task_queue.h index 720f4abffc..e7849fb198 100644 --- a/src/library/mt_task_queue.h +++ b/src/library/mt_task_queue.h @@ -32,7 +32,7 @@ class mt_task_queue : public task_queue { struct worker_info { thread m_thread; generic_task_result m_current_task; - atomic * m_interrupt_flag = nullptr; + atomic_bool * m_interrupt_flag = nullptr; }; std::vector> m_workers; bool m_shutting_down = false; diff --git a/src/library/versioned_msg_buf.cpp b/src/library/versioned_msg_buf.cpp index 08d1b508af..5a6fc2463d 100644 --- a/src/library/versioned_msg_buf.cpp +++ b/src/library/versioned_msg_buf.cpp @@ -7,7 +7,7 @@ Author: Gabriel Ebner #include #include #include -#include +#include "util/name_set.h" #include "library/versioned_msg_buf.h" #include "frontends/lean/info_manager.h" diff --git a/src/library/versioned_msg_buf.h b/src/library/versioned_msg_buf.h index c5e46cb82a..e27b6cd6e7 100644 --- a/src/library/versioned_msg_buf.h +++ b/src/library/versioned_msg_buf.h @@ -7,8 +7,8 @@ Author: Gabriel Ebner #pragma once #include #include -#include "library/message_buffer.h" #include "util/name.h" +#include "library/message_buffer.h" #include "frontends/lean/info_manager.h" namespace lean { diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index a0702de27c..f099bc4201 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -12,9 +12,6 @@ Author: Leonardo de Moura #include #include #include -#include -#include -#include "library/module_mgr.h" #include "util/realpath.h" #include "util/stackinfo.h" #include "util/macros.h" @@ -31,6 +28,9 @@ Author: Leonardo de Moura #include "kernel/kernel_exception.h" #include "kernel/type_checker.h" #include "kernel/formatter.h" +#include "library/st_task_queue.h" +#include "library/mt_task_queue.h" +#include "library/module_mgr.h" #include "library/standard_kernel.h" #include "library/module.h" #include "library/type_context.h" diff --git a/src/shell/server.cpp b/src/shell/server.cpp index c6be5643ed..7936f1476b 100644 --- a/src/shell/server.cpp +++ b/src/shell/server.cpp @@ -10,20 +10,20 @@ Authors: Gabriel Ebner, Leonardo de Moura, Sebastian Ullrich #include #include #include +#include "util/sexpr/option_declarations.h" +#include "util/bitap_fuzzy_search.h" +#include "kernel/instantiate.h" #include "library/mt_task_queue.h" #include "library/st_task_queue.h" -#include "frontends/lean/parser.h" -#include "library/module.h" -#include "shell/server.h" -#include "frontends/lean/info_manager.h" -#include "frontends/lean/definition_cmds.h" -#include "util/sexpr/option_declarations.h" -#include "frontends/lean/util.h" #include "library/protected.h" #include "library/scoped_ext.h" -#include "util/bitap_fuzzy_search.h" #include "library/type_context.h" -#include "kernel/instantiate.h" +#include "library/module.h" +#include "frontends/lean/parser.h" +#include "frontends/lean/info_manager.h" +#include "frontends/lean/definition_cmds.h" +#include "frontends/lean/util.h" +#include "shell/server.h" #ifndef LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS #define LEAN_DEFAULT_AUTO_COMPLETION_MAX_RESULTS 100 diff --git a/src/shell/server.h b/src/shell/server.h index bd17fafbe9..3425ea728a 100644 --- a/src/shell/server.h +++ b/src/shell/server.h @@ -5,13 +5,13 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Gabriel Ebner, Sebastian Ullrich */ #pragma once +#include #include "kernel/pos_info_provider.h" #include "kernel/environment.h" #include "library/io_state.h" -#include "frontends/lean/json.h" -#include #include "library/versioned_msg_buf.h" #include "library/module_mgr.h" +#include "frontends/lean/json.h" namespace lean { diff --git a/src/util/interrupt.cpp b/src/util/interrupt.cpp index 18b1a87c5e..97bcc2e1d8 100644 --- a/src/util/interrupt.cpp +++ b/src/util/interrupt.cpp @@ -51,7 +51,7 @@ void sleep_for(unsigned ms, unsigned step_ms) { check_interrupted(); } -atomic *get_interrupt_flag() { +atomic_bool * get_interrupt_flag() { return &get_g_interrupt(); } diff --git a/src/util/interrupt.h b/src/util/interrupt.h index 4cbc7fa53d..6b812b415c 100644 --- a/src/util/interrupt.h +++ b/src/util/interrupt.h @@ -11,8 +11,7 @@ Author: Leonardo de Moura #include "util/exception.h" namespace lean { - -atomic * get_interrupt_flag(); +atomic_bool * get_interrupt_flag(); /** \brief Mark flag for interrupting current thread.