more info

leanprover · Mar 5, 2024 · 0ddab02 · 0ddab02
1 parent 8ce1318
commit 0ddab02
Showing 1 changed file with 4 additions and 3 deletions.
diff --git 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