max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

feat: worker: don't abort on import error

Browse source 
to avoid the "crashed" message
This commit is contained in:
Sebastian Ullrich 2021-04-08 22:00:49 +02:00
parent c3d6f781cf
commit dd15c8d5a7
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Server/FileWorker.lean
View file

@ -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 := {