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

feat: auto-add stdlib to LEAN_SRC_PATH for installed Lean

Browse source
This commit is contained in:
Sebastian Ullrich 2021-01-21 14:12:51 +01:00
parent f0cbf08cb0
commit fbb1184f25
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -204,9 +204,9 @@ section Initialization
let leanpkgPath ← match ← IO.getEnv "LEAN_SYSROOT" with
| some path => s!"{path}/bin/leanpkg{System.FilePath.exeSuffix}"
| _ => s!"{← appDir}/leanpkg{System.FilePath.exeSuffix}"
let mut srcSearchPath := match (← IO.getEnv "LEAN_SRC_PATH") with
| some p => parseSearchPath p
| none => []
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