diff --git a/src/frontends/lean/CMakeLists.txt b/src/frontends/lean/CMakeLists.txt index 9f321b1127..db8d66163f 100644 --- a/src/frontends/lean/CMakeLists.txt +++ b/src/frontends/lean/CMakeLists.txt @@ -2,8 +2,7 @@ add_library(lean_frontend OBJECT tokens.cpp token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp parser.cpp builtin_cmds.cpp builtin_exprs.cpp notation_cmd.cpp decl_cmds.cpp util.cpp -inductive_cmds.cpp dependencies.cpp -pp.cpp structure_cmd.cpp structure_instance.cpp +inductive_cmds.cpp pp.cpp structure_cmd.cpp structure_instance.cpp init_module.cpp type_util.cpp decl_attributes.cpp prenum.cpp print_cmd.cpp elaborator.cpp match_expr.cpp local_context_adapter.cpp decl_util.cpp definition_cmds.cpp diff --git a/src/frontends/lean/dependencies.cpp b/src/frontends/lean/dependencies.cpp deleted file mode 100644 index 5eeed6569e..0000000000 --- a/src/frontends/lean/dependencies.cpp +++ /dev/null @@ -1,81 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include -#include -#include "runtime/sstream.h" -#include "util/lean_path.h" -#include "frontends/lean/scanner.h" - -namespace lean { - - -bool display_deps(search_path const & path, environment const & env, std::ostream & out, std::ostream & err, char const * fname) { - name import("import"); - name prelude("prelude"); - name period("."); - std::ifstream in(fname); - if (in.bad() || in.fail()) { - err << "failed to open file '" << fname << "'" << std::endl; - return false; - } - scanner s(in, fname); - optional k; - std::string base = dirname(fname); - bool import_prefix = false; - bool import_args = false; - bool ok = true; - bool is_prelude = false; - auto display_dep = [&](optional const & k, name const & f) { - import_args = true; - try { - std::string m_name = find_file(path, base, k, name_to_file(f), {".lean", ".hlean", ".olean", ".lua"}); - int last_idx = m_name.find_last_of("."); - std::string rawname = m_name.substr(0, last_idx); - std::string ext = m_name.substr(last_idx); - if (ext == ".lean" || ext == ".hlean") - m_name = rawname + ".olean"; - out << m_name; - import_prefix = true; - out << "\n"; - } catch (exception & new_ex) { - err << "error: file '" << name_to_file(s.get_name_val()) << "' not found in the LEAN_PATH" << std::endl; - ok = false; - } - }; - - while (true) { - token_kind t = token_kind::Identifier; - try { - t = s.scan(env); - } catch (exception &) { - continue; - } - if (t == token_kind::Eof) { - if (!is_prelude) - display_dep(optional(), name("init")); - return ok; - } else if (t == token_kind::CommandKeyword && s.get_token_info().value() == prelude) { - is_prelude = true; - } else if (t == token_kind::CommandKeyword && s.get_token_info().value() == import) { - k = optional(); - import_prefix = true; - } else if (import_prefix && t == token_kind::Keyword && s.get_token_info().value() == period) { - if (!k) - k = 0; - else - k = *k + 1; - } else if ((import_prefix || import_args) && t == token_kind::Identifier) { - display_dep(k, s.get_name_val()); - k = optional(); - } else { - import_args = false; - import_prefix = false; - } - } -} -} diff --git a/src/frontends/lean/dependencies.h b/src/frontends/lean/dependencies.h deleted file mode 100644 index 8d74800a99..0000000000 --- a/src/frontends/lean/dependencies.h +++ /dev/null @@ -1,13 +0,0 @@ -/* -Copyright (c) 2014 Microsoft Corporation. All rights reserved. -Released under Apache 2.0 license as described in the file LICENSE. - -Author: Leonardo de Moura -*/ -#include -#include "kernel/environment.h" - -namespace lean { -/** \brief Display in \c out all files the .lean file \c fname depends on */ -bool display_deps(search_path const &, environment const & env, std::ostream & out, std::ostream & err, char const * fname); -} diff --git a/src/frontends/lean/json.cpp b/src/frontends/lean/json.cpp index 1dc7d06609..1b3a39b122 100644 --- a/src/frontends/lean/json.cpp +++ b/src/frontends/lean/json.cpp @@ -10,6 +10,8 @@ Author: Gabriel Ebner #include "library/protected.h" #include "kernel/declaration.h" #include "library/type_context.h" +#include "library/protected.h" +#include "library/scoped_ext.h" #include "kernel/instantiate.h" #include "frontends/lean/pp.h" #include "frontends/lean/util.h" diff --git a/src/library/derive_attribute.cpp b/src/library/derive_attribute.cpp index ca064d4fb7..55785f5f9e 100644 --- a/src/library/derive_attribute.cpp +++ b/src/library/derive_attribute.cpp @@ -16,6 +16,7 @@ Author: Leonardo de Moura #include "library/type_context.h" #include "library/app_builder.h" #include "library/class.h" +#include "library/module.h" #include "library/protected.h" #include "library/sorry.h" diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 5af2be0e68..750942a245 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -39,7 +39,6 @@ Author: Leonardo de Moura #include "library/time_task.h" #include "frontends/lean/parser.h" #include "frontends/lean/pp.h" -#include "frontends/lean/dependencies.h" #include "frontends/lean/json.h" #include "frontends/lean/util.h" #include "library/trace.h" @@ -431,7 +430,6 @@ int main(int argc, char ** argv) { bool make_mode = false; bool recursive = false; unsigned trust_lvl = LEAN_BELIEVER_TRUST_LEVEL+1; - bool only_deps = false; bool test_suite = false; unsigned num_threads = 0; #if defined(LEAN_MULTI_THREAD) @@ -492,9 +490,6 @@ int main(int argc, char ** argv) { case 'q': opts = opts.update(lean::get_verbose_opt_name(), false); break; - case 'd': - only_deps = true; - break; case 'D': try { opts = set_config_option(opts, optarg); @@ -669,21 +664,6 @@ int main(int argc, char ** argv) { bool ok = true; - if (only_deps) { - for (auto & mod_fn : module_args) { - try { - if (!display_deps(path.get_path(), env, std::cout, std::cerr, mod_fn.c_str())) - ok = false; - } catch (lean::exception &ex) { - ok = false; - lean::message_builder(env, ios, mod_fn, lean::pos_info(1, 1), lean::ERROR).set_exception( - ex).report(); - } - } - - return ok ? 0 : 1; - } - struct input_mod { module_id m_id; std::shared_ptr m_mod_info;