fix: server: custom search path should win over package one should win over system one

I think that's all permutations now
This commit is contained in:
Sebastian Ullrich 2021-11-09 14:27:13 +01:00
parent a345a98ef7
commit 138d9eea43

View file

@ -173,8 +173,6 @@ section Initialization
let srcPath := (← appDir) / ".." / "lib" / "lean" / "src"
-- `lake/` should come first since on case-insensitive file systems, Lean thinks that `src/` also contains `Lake/`
let mut srcSearchPath := [srcPath / "lake", srcPath]
if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
srcSearchPath := System.SearchPath.parse p ++ srcSearchPath
let (headerEnv, msgLog) ← try
-- NOTE: lake does not exist in stage 0 (yet?)
if (← System.FilePath.pathExists lakePath) then
@ -184,6 +182,8 @@ section Initialization
catch e => -- should be from `lake print-paths`
let msgs := MessageLog.empty.add { fileName := "<ignored>", pos := ⟨0, 0⟩, data := e.toString }
pure (← mkEmptyEnvironment, msgs)
if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
srcSearchPath := System.SearchPath.parse p ++ srcSearchPath
let cmdState := Elab.Command.mkState headerEnv msgLog opts
let cmdState := { cmdState with infoState := {
enabled := true