perf: do not detect lean's toolchain

use `ELAN_TOOLCHAIN` only

src/lake/Lake/Config/Env.lean

@@ -51,13 +51,10 @@ def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstal
 
 /--
 The preferred toolchain of the environment. May be empty.
-Order is: `env.lean.toolchain` or `env.initToolchain` or Lake's `Lean.toolchain`
+Tries `env.initToolchain` first and then Lake's `Lean.toolchain`.
 -/
 def toolchain (env : Env) : String :=
-  if env.lean.toolchain.isEmpty then
-    if env.initToolchain.isEmpty then Lean.toolchain else env.initToolchain
-  else
-    env.lean.toolchain
+  if env.initToolchain.isEmpty then Lean.toolchain else env.initToolchain
 
 /--
 The binary search path of the environment (i.e., `PATH`).

src/lake/Lake/Config/InstallPath.lean

@@ -51,7 +51,6 @@ def leanSharedLib (sysroot : FilePath) :=
 structure LeanInstall where
   sysroot : FilePath
   githash : String
-  toolchain : String
   srcDir := sysroot / "src" / "lean"
   leanLibDir := sysroot / "lib" / "lean"
   includeDir := sysroot / "include"
@@ -158,22 +157,10 @@ Lean libraries in `<lean-sysroot>/lib/lean`, and its system libraries in
 -/
 def LeanInstall.get (sysroot : FilePath) : BaseIO LeanInstall := do
   let githash ← getGithash
-  let toolchain ← getToolchain
   let (cc, customCc) ← findCc
   let ar ← findAr
-  return {sysroot, githash, toolchain, ar, cc, customCc}
+  return {sysroot, githash, ar, cc, customCc}
 where
-  getToolchain := do
-    EIO.catchExceptions (h := fun _ => pure "") do
-      let child ← IO.Process.spawn {
-        cmd := leanExe sysroot |>.toString,
-        args := #["--stdin"],
-        stdout := .piped,
-        stdin := .piped,
-        stderr := .null
-      }
-      child.stdin.putStr "#eval IO.print Lean.toolchain"
-      pure <| (← child.stdout.getLine).trim
   getGithash := do
     EIO.catchExceptions (h := fun _ => pure "") do
       let out ← IO.Process.output {

src/lake/tests/env/test.sh

@@ -21,15 +21,8 @@ $LAKE env printenv LEAN_SRC_PATH | grep lake
 $LAKE -d ../../examples/hello env printenv LEAN_SRC_PATH | grep examples/hello
 $LAKE -d ../../examples/hello env printenv PATH | grep examples/hello
 
-# Test toolchain variable is set
-toolchain=`echo "#eval IO.print Lean.toolchain" | $LAKE env lean --stdin`
-if [ -n "$toolchain" ]; then
-  test "`$LAKE env printenv ELAN_TOOLCHAIN`" = "$toolchain"
-else
-  test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo
-fi
-
 # Test that `env` preserves the input environment for certain variables
+test "`$LAKE env env ELAN_TOOLCHAIN=foo $LAKE env printenv ELAN_TOOLCHAIN`" = foo
 test "`LEAN_AR=foo $LAKE env printenv LEAN_AR`" = foo
 test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo