From ddcc8de09e9752e66aeb13de7d3a755dba2fb55e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 15 Jan 2015 18:06:02 -0800 Subject: [PATCH] fix(shell/lean): catch errors when loading bad cache file --- src/shell/lean.cpp | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp index 05ac7e3383..7617a05a4b 100644 --- a/src/shell/lean.cpp +++ b/src/shell/lean.cpp @@ -483,10 +483,16 @@ int main(int argc, char ** argv) { definition_cache cache; definition_cache * cache_ptr = nullptr; if (use_cache) { - cache_ptr = &cache; - std::ifstream in(cache_name, std::ifstream::binary); - if (!in.bad() && !in.fail()) - cache.load(in); + try { + cache_ptr = &cache; + std::ifstream in(cache_name, std::ifstream::binary); + if (!in.bad() && !in.fail()) + cache.load(in); + } catch (lean::throwable & ex) { + lean::display_error(diagnostic(env, ios), nullptr, ex); + std::cerr << "Failed to load cache file '" << cache_name << "'\n"; + return 1; + } } declaration_index index; declaration_index * index_ptr = nullptr;