diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean index 41a0d08..52a7ac3 100644 --- a/src/examples/SubVerso/Examples.lean +++ b/src/examples/SubVerso/Examples.lean @@ -111,8 +111,9 @@ def findElanLake : IO String := do open System in partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example)) := do + let projectDir := ((โ† IO.currentDir) / leanProject).normalize -- Validate that the path is really a Lean project - let lakefile := leanProject / "lakefile.lean" + let lakefile := projectDir / "lakefile.lean" if !(โ† lakefile.pathExists) then throw <| .userError s!"File {lakefile} doesn't exist, couldn't load project" @@ -122,14 +123,14 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example let res โ† IO.Process.output { cmd := lake args := #["build", ":examples"] - cwd := leanProject + cwd := projectDir -- Unset Lake's environment variables env := #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP", "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH", "ELAN_TOOLCHAIN"].map (ยท, none) } if res.exitCode != 0 then IO.eprintln <| "Build process failed." ++ - "\nCWD: " ++ leanProject.toString ++ + "\nCWD: " ++ projectDir.toString ++ "\nCommand: " ++ lake ++ decorateOut "stdout" res.stdout ++ decorateOut "stderr" res.stderr