fix: unset Lake's environment variables for subproject invocations

leanprover · Mar 5, 2024 · acce30f · acce30f
1 parent 5052542
commit acce30f
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
@@ -101,6 +101,8 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example
     cmd := "lake"
     args := #["build", ":examples"]
     cwd := leanProject
+    -- Unset Lake's environment variables
+    env := #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP", "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH"].map (·, none)
   }
   if res.exitCode != 0 then
     throw <| .userError <|