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

feat: server: support LAKE env var

Browse source
This commit is contained in:
Sebastian Ullrich 2021-10-07 19:50:59 +02:00 • committed by Leonardo de Moura
parent e422ce4917
commit 674e473c84
1 changed files with 11 additions and 8 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -160,14 +160,17 @@ section Initialization
def compileHeader (m : DocumentMeta) (hOut : FS.Stream) (opts : Options) : IO (Snapshot × SearchPath) := do
let inputCtx := Parser.mkInputContext m.text.source "<input>"
let (headerStx, headerParserState, msgLog) ← Parser.parseHeader inputCtx
let lakePath :=
-- backward compatibility, kill when `leanpkg` is removed
if (← System.FilePath.pathExists "leanpkg.toml") && !(← System.FilePath.pathExists "lakefile.lean") then "leanpkg"
else "lake"
let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with
| some path => pure <| System.FilePath.mk path / "bin" / lakePath
| _ => pure <| (← appDir) / lakePath
let lakePath := lakePath.withExtension System.FilePath.exeExtension
let lakePath ← match (← IO.getEnv "LAKE") with
| some path => System.FilePath.mk path
| none =>
let lakePath :=
-- backward compatibility, kill when `leanpkg` is removed
if (← System.FilePath.pathExists "leanpkg.toml") && !(← System.FilePath.pathExists "lakefile.lean") then "leanpkg"
else "lake"
let lakePath ← match (← IO.getEnv "LEAN_SYSROOT") with
| some path => pure <| System.FilePath.mk path / "bin" / lakePath
| _ => pure <| (← appDir) / lakePath
lakePath.withExtension System.FilePath.exeExtension
let mut srcSearchPath := [(← appDir) / ".." / "lib" / "lean" / "src"]
if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
srcSearchPath := srcSearchPath ++ System.SearchPath.parse p