From dd15c8d5a7fbda0099398de397f9f07538c0c035 Mon Sep 17 00:00:00 2001
From: Sebastian Ullrich <sebasti@nullri.ch>
Date: Thu, 8 Apr 2021 22:00:49 +0200
Subject: [PATCH] feat: worker: don't abort on import error

to avoid the "crashed" message
---
 src/Lean/Server/FileWorker.lean | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean
index 3407efff41..bbb0560fc1 100644
--- a/src/Lean/Server/FileWorker.lean
+++ b/src/Lean/Server/FileWorker.lean
@@ -215,11 +215,14 @@ section Initialization
     let mut srcSearchPath := [s!"{← appDir}/../lib/lean/src"]
     if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
       srcSearchPath := srcSearchPath ++ parseSearchPath p
-    -- NOTE: leanpkg does not exist in stage 0 (yet?)
-    if (← fileExists leanpkgPath) then
-      let pkgSearchPath ← leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray hOut
-      srcSearchPath := srcSearchPath ++ pkgSearchPath
-    let (headerEnv, msgLog) ← Elab.processHeader headerStx opts msgLog inputCtx
+    let (headerEnv, msgLog) ← try
+      -- NOTE: leanpkg does not exist in stage 0 (yet?)
+      if (← fileExists leanpkgPath) then
+        let pkgSearchPath ← leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray hOut
+        srcSearchPath := srcSearchPath ++ pkgSearchPath
+      Elab.processHeader headerStx opts msgLog inputCtx
+    catch e =>  -- should be from `leanpkg print-paths`
+      pure (← mkEmptyEnvironment, MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString })
     let cmdState := Elab.Command.mkState headerEnv msgLog opts
     let cmdState := { cmdState with infoState.enabled := true, scopes := [{ header := "", opts := opts }] }
     let headerSnap := {