From db81e4b5b8f60fed9e11dfd2fda9f31c996e4686 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Thu, 12 Jan 2017 08:12:59 +0100
Subject: [PATCH] feat(frontends/lean/parser): gracefully handle scanner
 exceptions in imports

---
 src/frontends/lean/parser.cpp                 | 19 +++++++++++++------
 src/frontends/lean/parser.h                   |  4 ++--
 src/library/module_mgr.cpp                    | 10 +++++-----
 tests/lean/import_invalid_tk.lean             |  3 +++
 .../lean/import_invalid_tk.lean.expected.out  |  4 ++++
 5 files changed, 27 insertions(+), 13 deletions(-)
 create mode 100644 tests/lean/import_invalid_tk.lean
 create mode 100644 tests/lean/import_invalid_tk.lean.expected.out

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index bc06f2bc18..82b5dc7158 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2111,14 +2111,13 @@ void parser::reset_doc_string() {
 #pragma GCC diagnostic ignored "-Wmaybe-uninitialized"
 #endif
 
-std::vector<module_name> parser::parse_imports(unsigned & fingerprint) {
+void parser::parse_imports(unsigned & fingerprint, std::vector<module_name> & imports) {
     m_last_cmd_pos = pos();
     bool prelude     = false;
     if (curr_is_token(get_prelude_tk())) {
         next();
         prelude = true;
     }
-    std::vector<module_name> imports;
     if (!prelude) {
         imports.push_back({ "init", optional<unsigned>() });
     }
@@ -2171,12 +2170,18 @@ std::vector<module_name> parser::parse_imports(unsigned & fingerprint) {
             }
         }
     }
-    return imports;
 }
 
 void parser::process_imports() {
     unsigned fingerprint = 0;
-    auto imports = parse_imports(fingerprint);
+    std::vector<module_name> imports;
+
+    std::exception_ptr exception_during_scanning;
+    try {
+        parse_imports(fingerprint, imports);
+    } catch (parser_exception) {
+        exception_during_scanning = std::current_exception();
+    }
 
     buffer<import_error> import_errors;
     m_env = import_modules(m_env, m_file_name, imports, m_import_fn, import_errors);
@@ -2209,12 +2214,14 @@ void parser::process_imports() {
 #endif
     }
     m_imports_parsed = true;
+
+    if (exception_during_scanning) std::rethrow_exception(exception_during_scanning);
 }
 
-std::vector<module_name> parser::get_imports() {
+void parser::get_imports(std::vector<module_name> & imports) {
     scope_pos_info_provider scope1(*this);
     unsigned fingerprint;
-    return parse_imports(fingerprint);
+    parse_imports(fingerprint, imports);
 }
 
 bool parser::parse_commands() {
diff --git a/src/frontends/lean/parser.h b/src/frontends/lean/parser.h
index 7828a8de1a..d99b2a60f5 100644
--- a/src/frontends/lean/parser.h
+++ b/src/frontends/lean/parser.h
@@ -431,7 +431,7 @@ public:
 
     expr parse_tactic(unsigned rbp = 0);
 
-    std::vector<module_name> parse_imports(unsigned & fingerprint);
+    void parse_imports(unsigned & fingerprint, std::vector<module_name> &);
 
     struct local_scope {
         parser & m_p; environment m_env;
@@ -522,7 +522,7 @@ public:
     /** parse all commands in the input stream */
     bool operator()() { return parse_commands(); }
 
-    std::vector<module_name> get_imports();
+    void get_imports(std::vector<module_name> &);
 
     class in_notation_ctx {
         scanner::in_notation_ctx m_ctx;
diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index ad2b166226..d7a68bd299 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -404,16 +404,16 @@ module_mgr::get_snapshots_or_unchanged_module(module_id const &id, std::string c
 }
 
 std::vector<module_name> module_mgr::get_direct_imports(module_id const & id, std::string const & contents) {
+    std::vector<module_name> imports;
     try {
         scope_message_context scope("dependencies");
         std::istringstream in(contents);
         bool use_exceptions = true;
         parser p(get_initial_env(), m_ios, nullptr, in, id, use_exceptions);
-        std::vector<std::pair<module_name, module_id>> deps;
-        return p.get_imports();
-    } catch (...) {
-        return {};
-    }
+        p.get_imports(imports);
+    } catch (...) {}
+
+    return imports;
 }
 
 std::tuple<std::string, module_src, time_t> fs_module_vfs::load_module(module_id const & id, bool can_use_olean) {
diff --git a/tests/lean/import_invalid_tk.lean b/tests/lean/import_invalid_tk.lean
new file mode 100644
index 0000000000..5ff4c774c4
--- /dev/null
+++ b/tests/lean/import_invalid_tk.lean
@@ -0,0 +1,3 @@
+import data.bitvec 0b311
+
+print bitvec
diff --git a/tests/lean/import_invalid_tk.lean.expected.out b/tests/lean/import_invalid_tk.lean.expected.out
new file mode 100644
index 0000000000..ba86b12e6f
--- /dev/null
+++ b/tests/lean/import_invalid_tk.lean.expected.out
@@ -0,0 +1,4 @@
+import_invalid_tk.lean:1:21: error: invalid binary digit
+attribute [reducible]
+definition bitvec : ℕ → Type :=
+λ (n : ℕ), tuple bool n