From 40f7ef5097bdfd15d87ec5b9544b220cf4a307a4 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 14 Aug 2014 15:47:46 -0700 Subject: [PATCH] feat(shell/lean): display src file name when printing 'file not found in the LEAN_PATH' error, closes #47 Signed-off-by: Leonardo de Moura --- src/library/error_handling/error_handling.cpp | 4 +- src/shell/lean.cpp | 58 ++++++++++++------- src/util/lean_path.cpp | 9 ++- src/util/lean_path.h | 8 +++ 4 files changed, 54 insertions(+), 25 deletions(-) diff --git a/src/library/error_handling/error_handling.cpp b/src/library/error_handling/error_handling.cpp index 2b18cb7e4..3023364e8 100644 --- a/src/library/error_handling/error_handling.cpp +++ b/src/library/error_handling/error_handling.cpp @@ -35,7 +35,9 @@ flyinfo_scope::~flyinfo_scope() { } void display_pos(io_state_stream const & ios, char const * strm_name, unsigned line, unsigned pos) { - ios << strm_name << ":" << line << ":"; + ios << strm_name << ":"; + if (line != static_cast(-1)) + ios << line << ":"; if (pos != static_cast(-1)) ios << pos << ":"; } diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 005d6beab..c1a4903fa 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -45,6 +45,10 @@ using lean::mk_hott_environment; using lean::set_environment; using lean::set_io_state; using lean::definitions_cache; +using lean::pos_info; +using lean::pos_info_provider; +using lean::optional; +using lean::expr; enum class input_kind { Unspecified, Lean, Lua }; @@ -131,6 +135,15 @@ static char const * g_opt_str = "PFDHSqlupgvhj:012k:012t:012o:c:"; enum class lean_mode { Standard, HoTT }; +class simple_pos_info_provider : public pos_info_provider { + char const * m_fname; +public: + simple_pos_info_provider(char const * fname):m_fname(fname) {} + virtual optional get_pos_info(expr const &) const { return optional(); } + virtual char const * get_file_name() const { return m_fname; } + virtual pos_info get_some_pos() const { return pos_info(-1, -1); } +}; + int main(int argc, char ** argv) { lean::save_stack_info(); lean::register_modules(); @@ -237,30 +250,31 @@ int main(int argc, char ** argv) { try { bool ok = true; for (int i = optind; i < argc; i++) { - char const * ext = get_file_extension(argv[i]); - input_kind k = default_k; - if (ext) { - if (strcmp(ext, "lean") == 0) { - k = input_kind::Lean; - } else if (strcmp(ext, "lua") == 0) { - k = input_kind::Lua; + try { + char const * ext = get_file_extension(argv[i]); + input_kind k = default_k; + if (ext) { + if (strcmp(ext, "lean") == 0) { + k = input_kind::Lean; + } else if (strcmp(ext, "lua") == 0) { + k = input_kind::Lua; + } } - } - if (k == input_kind::Lean) { - if (only_deps) { - display_deps(env, std::cout, argv[i]); - } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr)) { - ok = false; - } - } else if (k == input_kind::Lua) { - try { + if (k == input_kind::Lean) { + if (only_deps) { + display_deps(env, std::cout, argv[i]); + } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr)) { + ok = false; + } + } else if (k == input_kind::Lua) { lean::system_import(argv[i]); - } catch (lean::exception & ex) { - ::lean::display_error(regular(env, ios), nullptr, ex); - ok = false; + } else { + lean_unreachable(); // LCOV_EXCL_LINE } - } else { - lean_unreachable(); // LCOV_EXCL_LINE + } catch (lean::exception & ex) { + simple_pos_info_provider pp(argv[i]); + ok = false; + lean::display_error(diagnostic(env, ios), &pp, ex); } } if (ok && server && default_k == input_kind::Lean) { @@ -279,7 +293,7 @@ int main(int argc, char ** argv) { } return ok ? 0 : 1; } catch (lean::exception & ex) { - ::lean::display_error(diagnostic(env, ios), nullptr, ex); + lean::display_error(diagnostic(env, ios), nullptr, ex); } return 1; } diff --git a/src/util/lean_path.cpp b/src/util/lean_path.cpp index 8ffb74b31..1d960abb5 100644 --- a/src/util/lean_path.cpp +++ b/src/util/lean_path.cpp @@ -15,12 +15,17 @@ Author: Leonardo de Moura #include "util/name.h" #include "util/optional.h" #include "util/realpath.h" +#include "util/lean_path.h" #ifndef LEAN_DEFAULT_MODULE_FILE_NAME #define LEAN_DEFAULT_MODULE_FILE_NAME "default" #endif namespace lean { +file_not_found_exception::file_not_found_exception(std::string const & fname): + exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH"), + m_fname(fname) {} + static std::string g_default_file_name(LEAN_DEFAULT_MODULE_FILE_NAME); bool is_directory(char const * pathname) { @@ -186,7 +191,7 @@ std::string find_file(std::string fname, std::initializer_list con } } } - throw exception(sstream() << "file '" << fname << "' not found in the LEAN_PATH"); + throw file_not_found_exception(fname); } std::string find_file(std::string const & base, optional const & rel, name const & fname, @@ -203,7 +208,7 @@ std::string find_file(std::string const & base, optional const & rel, if (auto r = check_file(path, fname.to_string(g_sep_str.c_str()), ext)) return *r; } - throw exception(sstream() << "file '" << fname << "' not found at '" << path << "'"); + throw file_not_found_exception(fname.to_string()); } } diff --git a/src/util/lean_path.h b/src/util/lean_path.h index 358f28450..40a246e1b 100644 --- a/src/util/lean_path.h +++ b/src/util/lean_path.h @@ -7,7 +7,15 @@ Author: Leonardo de Moura #pragma once #include #include "util/name.h" +#include "util/exception.h" + namespace lean { +class file_not_found_exception : public exception { + std::string m_fname; +public: + file_not_found_exception(std::string const & fname); +}; + /** \brief Initialize the lean_path for the given kernel instance */ void init_lean_path(char const * kernel_instance_name); /** \brief Return the LEAN_PATH string */