Improve error handling

src/frontends/lean/parser.cpp

@@ -181,8 +181,11 @@ void parser::updt_options() {
 
 void parser::sync_command() {
     // Keep consuming tokens until we find a Command or End-of-file
-    while (curr() != token_kind::CommandKeyword && curr() != token_kind::Eof)
-        next();
+    while (curr() != token_kind::CommandKeyword && curr() != token_kind::Eof) {
+        try {
+            next();
+        } catch (parser_exception const &) {}
+    }
 }
 
 name parser::mk_anonymous_inst_name() {

src/library/messages.cpp

@@ -34,7 +34,7 @@ std::ostream & operator<<(std::ostream & out, message const & msg) {
 void report_message(message const & msg0) {
     if (!get_global_ios().get_options().get_bool(name {"trace", "as_messages"}, false)) {
         // Print immediately. Still add as a message so that we get the error code correct.
-        get_global_ios().get_regular_stream() << msg0;
+        get_global_ios().get_diagnostic_stream() << msg0;
     }
     lean_assert(global_message_log());
     global_message_log()->add(msg0);

src/shell/lean.cpp

@@ -562,41 +562,45 @@ int main(int argc, char ** argv) {
             scope_traces_as_messages scope_trace_msgs(mod_fn, {1, 0});
             simple_pos_info_provider pip(mod_fn.c_str());
             scope_pos_info_provider scope_pip(pip);
-
-            // TODO(Sebastian): parse imports using new frontend
+            message_log l;
+            scope_message_log scope_log(l);
             std::vector<rel_module_name> rel_imports;
             std::istringstream in(contents);
             parser p(env, ios, in, mod_fn);
-            p.parse_imports(rel_imports);
-
-            std::vector<module_name> imports;
-            auto dir = dirname(mod_fn);
-            for (auto const & rel : rel_imports)
-                imports.push_back(absolutize_module_name(path, dir, rel));
-
-            if (only_deps) {
-                for (auto const & import : imports) {
-                    std::string m_name = find_lean_file(import);
-                    auto last_idx = m_name.find_last_of(".");
-                    std::string rawname = m_name.substr(0, last_idx);
-                    std::string ext = m_name.substr(last_idx);
-                    m_name = rawname + ".olean";
-                    std::cout << m_name << "\n";
+
+            try {
+                p.parse_imports(rel_imports);
+
+                std::vector<module_name> imports;
+                auto dir = dirname(mod_fn);
+                for (auto const & rel : rel_imports)
+                    imports.push_back(absolutize_module_name(path, dir, rel));
+
+                if (only_deps) {
+                    for (auto const & import : imports) {
+                        std::string m_name = find_lean_file(import);
+                        auto last_idx = m_name.find_last_of(".");
+                        std::string rawname = m_name.substr(0, last_idx);
+                        std::string ext = m_name.substr(last_idx);
+                        m_name = rawname + ".olean";
+                        std::cout << m_name << "\n";
+                    }
+                    return 0;
                 }
-                return 0;
-            }
 
-            message_log l;
-            scope_message_log scope_log(l);
-            if (stats) {
-                timeit timer(std::cout, "import");
-                env = import_modules(trust_lvl, imports);
-            } else {
-                env = import_modules(trust_lvl, imports);
+                if (stats) {
+                    timeit timer(std::cout, "import");
+                    env = import_modules(trust_lvl, imports);
+                } else {
+                    env = import_modules(trust_lvl, imports);
+                }
+                env.set_main_module(main_module_name);
+                p.set_env(env);
+                p.parse_commands();
+            } catch (lean::throwable & ex) {
+                report_message(lean::message_builder(env, ios, mod_fn, lean::pos_info(1, 1), lean::ERROR)
+                                       .set_exception(ex).build());
             }
-            env.set_main_module(main_module_name);
-            p.set_env(env);
-            p.parse_commands();
 
             if (json_output) {
 #if defined(LEAN_JSON)

tests/lean/test_single.sh

@@ -26,7 +26,7 @@ if diff --color --help >/dev/null 2>&1; then
 fi
 
 echo "-- testing $f"
-"$LEAN" "$ff" | sed 's|does\\not\\exist|does/not/exist|' | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out"
+"$LEAN" "$ff" 2>&1 | sed 's|does\\not\\exist|does/not/exist|' | sed "/warning: imported file uses 'sorry'/d" | sed "/warning: using 'sorry'/d" | sed "/failed to elaborate theorem/d" | sed "s|^$ff|$f|" > "$f.produced.out"
 if test -f "$f.expected.out"; then
     if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
         echo "-- checked"

tests/plugin/test_single.sh

@@ -37,7 +37,7 @@ if [ $? -ne 0 ]; then
     exit 1
 fi
 
-$BIN_DIR/lean --plugin="$ff.so" "$ff" | sed "s|^$ff|$f|" > "$f.produced.out"
+$BIN_DIR/lean --plugin="$ff.so" "$ff" 2>&1 | sed "s|^$ff|$f|" > "$f.produced.out"
 if test -f "$f.expected.out"; then
     if $DIFF -u --ignore-all-space -I "executing external script" "$f.expected.out" "$f.produced.out"; then
         echo "-- checked"