From 138d9eea43bec287d53bbb9a2ecb2ba0d6ead221 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 9 Nov 2021 14:27:13 +0100 Subject: [PATCH] fix: server: custom search path should win over package one should win over system one I think that's all permutations now --- src/Lean/Server/FileWorker.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Lean/Server/FileWorker.lean b/src/Lean/Server/FileWorker.lean index 51fda06da0..4d086cf813 100644 --- a/src/Lean/Server/FileWorker.lean +++ b/src/Lean/Server/FileWorker.lean @@ -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 := "", 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