From 5ff62ebf0614ed70dd5eb5cd4ea97074b99fa73a Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 5 Feb 2020 09:42:26 -0800
Subject: [PATCH] feat: check user given path

---
 src/Init/Lean/Util/Path.lean | 5 ++++-
 src/shell/lean.cpp           | 7 ++++++-
 2 files changed, 10 insertions(+), 2 deletions(-)

diff --git a/src/Init/Lean/Util/Path.lean b/src/Init/Lean/Util/Path.lean
index 964bbafe9b..d032ba6fea 100644
--- a/src/Init/Lean/Util/Path.lean
+++ b/src/Init/Lean/Util/Path.lean
@@ -38,7 +38,10 @@ constant searchPathRef : IO.Ref SearchPath := arbitrary _
 def parseSearchPath (path : String) (sp : SearchPath := ∅) : IO SearchPath := do
 let ps := System.FilePath.splitSearchPath path;
 sp ← ps.foldlM (fun (sp : SearchPath) s => match s.splitOn "=" with
-  | [pkg, path] => pure $ sp.insert pkg path
+  | [pkg, path] => do
+    condM (IO.isDir path)
+      (pure $ sp.insert pkg path)
+      (throw $ IO.userError $ "invalid search path, '" ++ path ++ "' is not a directory")
   | _           => throw $ IO.userError $ "ill-formed search path entry '" ++ s ++ "', should be of form 'pkg=path'")
   sp;
 pure sp
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 3aa1be8c8a..8ad7f64471 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -427,7 +427,12 @@ int main(int argc, char ** argv) {
     llvm::InitializeNativeTarget();
 #endif
 
-    init_search_path();
+    try {
+        init_search_path();
+    } catch (lean::throwable & ex) {
+        std::cerr << "error: " << ex.what() << std::endl;
+        return 1;
+    }
 
     options opts;
     optional<std::string> server_in;