diff --git a/demo/lakefile.lean b/demo/lakefile.lean
index f613568..59cf3c0 100644
--- a/demo/lakefile.lean
+++ b/demo/lakefile.lean
@@ -1,7 +1,11 @@
 import Lake
 open Lake DSL
 
-require subverso from ".."
+-- This needs to be git rather than a filesystem path, because git
+-- will clone the project. This results in a separate .lake build dir,
+-- so the different versions of Lake don't stomp on each others'
+-- files.
+require subverso from git ".."
 
 package «demo» where
   -- add package configuration options here
diff --git a/lean-toolchain b/lean-toolchain
index 6ff4890..63510c1 100644
--- a/lean-toolchain
+++ b/lean-toolchain
@@ -1 +1 @@
-leanprover/lean4:nightly-2024-02-26
+leanprover/lean4:4.6.0
diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean
index b80a3d4..90e3e16 100644
--- a/src/examples/SubVerso/Examples.lean
+++ b/src/examples/SubVerso/Examples.lean
@@ -117,6 +117,17 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example
   if !(← lakefile.pathExists) then
     throw <| .userError s!"File {lakefile} doesn't exist, couldn't load project"
 
+  -- Kludge: path entries likely added by Elan
+  let newpath := System.SearchPath.parse ((← IO.getEnv "PATH").getD "") |>.filter ("toolchains" ∉ ·.toString.splitOn "/")
+
+  -- Kludge: remove variables introduced by Lake. Clearing out DYLD_LIBRARY_PATH and
+  -- LD_LIBRARY_PATH is useful so the version selected by Elan doesn't get the wrong shared
+  -- libraries.
+  let lakeVars :=
+    #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP",
+      "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH",
+      "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"]
+
   let lake ← findElanLake
 
   -- Build the facet
@@ -125,7 +136,7 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example
     args := #["build", ":examples"]
     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)
+    env := lakeVars.map (·, none)
   }
   if res.exitCode != 0 then
     IO.eprintln <|