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 <leonardo@microsoft.com>

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<unsigned>(-1))
+        ios << line << ":";
     if (pos != static_cast<unsigned>(-1))
         ios << pos << ":";
 }

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<pos_info> get_pos_info(expr const &) const { return optional<pos_info>(); }
+    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]);
+            try {
-            input_kind k     = default_k;
+                char const * ext = get_file_extension(argv[i]);
-            if (ext) {
+                input_kind k     = default_k;
-                if (strcmp(ext, "lean") == 0) {
+                if (ext) {
-                    k = input_kind::Lean;
+                    if (strcmp(ext, "lean") == 0) {
-                } else if (strcmp(ext, "lua") == 0) {
+                        k = input_kind::Lean;
-                    k = input_kind::Lua;
+                    } else if (strcmp(ext, "lua") == 0) {
+                        k = input_kind::Lua;
+                    }
                 }
-            }
+                if (k == input_kind::Lean) {
-            if (k == input_kind::Lean) {
+                    if (only_deps) {
-                if (only_deps) {
+                        display_deps(env, std::cout, argv[i]);
-                    display_deps(env, std::cout, argv[i]);
+                    } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr)) {
-                } else if (!parse_commands(env, ios, argv[i], false, num_threads, cache_ptr)) {
+                        ok = false;
-                    ok = false;
+                    }
-                }
+                } else if (k == input_kind::Lua) {
-            } else if (k == input_kind::Lua) {
-                try {
                     lean::system_import(argv[i]);
-                } catch (lean::exception & ex) {
+                } else {
-                    ::lean::display_error(regular(env, ios), nullptr, ex);
+                    lean_unreachable(); // LCOV_EXCL_LINE
-                    ok = false;
                 }
-            } else {
+            } catch (lean::exception & ex) {
-                lean_unreachable(); // LCOV_EXCL_LINE
+                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;
 }

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<char const *> 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<unsigned> const & rel, name const & fname,
@@ -203,7 +208,7 @@ std::string find_file(std::string const & base, optional<unsigned> 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());
     }
 }
 

src/util/lean_path.h

@@ -7,7 +7,15 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #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 */