fix: run Lean subprocesses correctly

This allows the tests to pass locally and on CI

.github/workflows/ci.yml

@@ -22,6 +22,11 @@ jobs:
           curl -sSfL https://github.com/leanprover/elan/releases/download/v3.0.0/elan-x86_64-unknown-linux-gnu.tar.gz | tar xz
           ./elan-init -y --default-toolchain none
           echo "$HOME/.elan/bin" >> $GITHUB_PATH
+
+      - name: Which lake?
+        run: |
+          which lake
+
       - uses: actions/checkout@v3
 
       - name: List all files
@@ -49,7 +54,8 @@ jobs:
       - name: Configure demo/test subproject
         run: |
           pushd demo
-          lake update
+          ~/.elan/bin/lake update
+          ~/.elan/bin/lake build :examples
           popd
 
       - name: Run tests

Tests.lean

@@ -6,13 +6,10 @@ import Lean
 open SubVerso.Examples (loadExamples Example)
 open Lean.FromJson (fromJson?)
 
-def assert (what : String) (cond : Unit -> Bool) : IO Unit := do
-  if !(cond ()) then
-    throw <| .userError what
-
-
 def main : IO UInt32 := do
   IO.println "Checking that the test project generates at least some deserializable JSON"
   let examples ← loadExamples "demo"
-  assert "Examples are non-empty" fun () => !examples.isEmpty
+  if examples.isEmpty then
+    IO.eprintln "No examples found"
+    return 1
   pure 0

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

lean-toolchain

@@ -1 +1 @@
-leanprover/lean4:nightly-2024-02-26
+leanprover/lean4:4.6.0

src/examples/SubVerso/Examples.lean

@@ -111,20 +111,42 @@ 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"
 
+  -- 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
   let res ← IO.Process.output {
-    cmd := ← findElanLake
+    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)
+    env := lakeVars.map (·, none)
   }
   if res.exitCode != 0 then
+    IO.eprintln <|
+      "Build process failed." ++
+      "\nCWD: " ++ projectDir.toString ++
+      "\nCommand: " ++ lake ++
+      "\nExit code: " ++ toString res.exitCode ++
+      "\nstdout: " ++ res.stdout ++
+      "\nstderr: " ++ res.stderr
+
     throw <| .userError <|
       "Build process failed." ++
       decorateOut "stdout" res.stdout ++