From 01a7efc0076daa398d90be6b8a4544905d0372fb Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Tue, 4 Apr 2017 19:56:33 +0200
Subject: [PATCH] fix(library/module_mgr): do not crash on missing imports

Fixes #1506.
---
 src/frontends/lean/parser.cpp                        |  2 +-
 src/library/module_mgr.cpp                           |  3 ++-
 .../interactive/complete_import.lean.expected.out    | 12 ++++++------
 tests/lean/missing_import.lean.expected.out          |  1 -
 4 files changed, 9 insertions(+), 9 deletions(-)

diff --git a/src/frontends/lean/parser.cpp b/src/frontends/lean/parser.cpp
index 233ba73252..7f5bd27e90 100644
--- a/src/frontends/lean/parser.cpp
+++ b/src/frontends/lean/parser.cpp
@@ -2297,7 +2297,7 @@ void parser::process_imports() {
             try {
                 std::rethrow_exception(e.m_ex);
             } catch (throwable & t) {
-                parser_exception error((sstream() << "invalid import: " << e.m_import.m_name << "\n" << t.what()).str(),
+                parser_exception error((sstream() << "invalid import: " << e.m_import.m_name).str(),
                                        m_file_name.c_str(), m_last_cmd_pos);
                 if (!m_use_exceptions && m_show_errors)
                     report_message(error);
diff --git a/src/library/module_mgr.cpp b/src/library/module_mgr.cpp
index f1944e2065..e506584412 100644
--- a/src/library/module_mgr.cpp
+++ b/src/library/module_mgr.cpp
@@ -83,7 +83,8 @@ static gtask compile_olean(std::shared_ptr<module_info const> const & mod, log_t
 
     std::vector<gtask> olean_deps;
     for (auto & dep : mod->m_deps)
-        olean_deps.push_back(dep.m_mod_info->m_olean_task);
+        if (dep.m_mod_info)
+            olean_deps.push_back(dep.m_mod_info->m_olean_task);
 
     return add_library_task(task_builder<unit>([mod, errs] {
         if (mod->m_source != module_src::LEAN)
diff --git a/tests/lean/interactive/complete_import.lean.expected.out b/tests/lean/interactive/complete_import.lean.expected.out
index b6e2483714..8cb590d791 100644
--- a/tests/lean/interactive/complete_import.lean.expected.out
+++ b/tests/lean/interactive/complete_import.lean.expected.out
@@ -4,12 +4,12 @@
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"}],"response":"all_messages"}
 {"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"}],"response":"all_messages"}
-{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo\ncould not resolve import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: bar\ncould not resolve import: bar"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"}],"response":"all_messages"}
+{"msgs":[{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'foo' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":1,"severity":"error","text":"file 'bar' not found in the LEAN_PATH"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: foo"},{"caption":"","file_name":"f","pos_col":0,"pos_line":17,"severity":"error","text":"invalid import: bar"}],"response":"all_messages"}
 {"message":"file invalidated","response":"ok","seq_num":0}
 {"response":"ok","seq_num":2}
 {"prefix":"","response":"ok","seq_num":4}
diff --git a/tests/lean/missing_import.lean.expected.out b/tests/lean/missing_import.lean.expected.out
index 5b81f13964..3c9e9f2493 100644
--- a/tests/lean/missing_import.lean.expected.out
+++ b/tests/lean/missing_import.lean.expected.out
@@ -1,6 +1,5 @@
 missing_import.lean:1:0: error: file 'does/not/exist' not found in the LEAN_PATH
 missing_import.lean:1:0: error: invalid import: does.not.exist
-could not resolve import: does.not.exist
 @[reducible]
 def bitvec : ℕ → Type :=
 λ (n : ℕ), vector bool n