From 4a075f4f1c5a9925090319ec087cffaf931e9674 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 17 Apr 2024 11:21:41 +0200 Subject: [PATCH 1/4] fix: simply use lake from PATH, avoid cleverness --- src/examples/SubVerso/Examples.lean | 32 +++++------------------------ 1 file changed, 5 insertions(+), 27 deletions(-) diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean index b6a0b19..dc4be0d 100644 --- a/src/examples/SubVerso/Examples.lean +++ b/src/examples/SubVerso/Examples.lean @@ -148,25 +148,6 @@ elab_rules : command else throwErrorAt name "No highlighting found for '{name}'" -def findElanLake : IO String := do - if let some elanPath ← IO.getEnv "ELAN_HOME" then - return ((elanPath : System.FilePath) / "bin" / "lake").toString - let some path ← IO.getEnv "PATH" - | return "lake" -- better than crashing! - let entries := System.SearchPath.parse path - for entry in entries do - -- This is an elan version of lake if it responds well to a `+` - let lakePath := entry / "lake" - let out ← IO.Process.output { - cmd := lakePath.toString - args := #["+stable"] - cwd := entry - env := #["LAKE", "LAKE_HOME", "LAKE_PKG_URL_MAP", "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH", "ELAN_TOOLCHAIN"].map (·, none) - } - if out.exitCode == 0 then - return lakePath.toString - return "lake" - open System in partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example)) := do let projectDir := ((← IO.currentDir) / leanProject).normalize @@ -175,9 +156,6 @@ 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. @@ -186,13 +164,12 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH", "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"] - let lake ← findElanLake + let cmd := "lake" + let args := #["build", ":examples"] -- Build the facet let res ← IO.Process.output { - cmd := lake - args := #["build", ":examples"] - cwd := projectDir + cmd, args, cwd := projectDir -- Unset Lake's environment variables env := lakeVars.map (·, none) } @@ -200,7 +177,8 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example IO.eprintln <| "Build process failed." ++ "\nCWD: " ++ projectDir.toString ++ - "\nCommand: " ++ lake ++ + "\nCommand: " ++ cmd ++ + "\nArgs: " ++ repr args ++ "\nExit code: " ++ toString res.exitCode ++ "\nstdout: " ++ res.stdout ++ "\nstderr: " ++ res.stderr From 9a171eff7e84737acf5cea097d4a0b9393ba8194 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 17 Apr 2024 14:29:44 +0200 Subject: [PATCH 2/4] Invoke elan, not lake --- src/examples/SubVerso/Examples.lean | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean index dc4be0d..e412185 100644 --- a/src/examples/SubVerso/Examples.lean +++ b/src/examples/SubVerso/Examples.lean @@ -155,6 +155,10 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example let lakefile := projectDir / "lakefile.lean" if !(← lakefile.pathExists) then throw <| .userError s!"File {lakefile} doesn't exist, couldn't load project" + let toolchainfile := projectDir / "lean-toolchain" + if !(← toolchainfile.pathExists) then + throw <| .userError s!"File {toolchainfile} doesn't exist, couldn't load project" + let toolchain := ← IO.FS.readFile toolchainfile -- 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 @@ -164,8 +168,8 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example "LEAN_SYSROOT", "LEAN_AR", "LEAN_PATH", "LEAN_SRC_PATH", "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"] - let cmd := "lake" - let args := #["build", ":examples"] + let cmd := "elan" + let args := #["run", toolchain, "lake", "build", ":examples"] -- Build the facet let res ← IO.Process.output { From d433172f093c0c1a2760efabcd166cf7c2fa05f8 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 17 Apr 2024 14:31:05 +0200 Subject: [PATCH 3/4] Pass --install --- src/examples/SubVerso/Examples.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean index e412185..74dc74c 100644 --- a/src/examples/SubVerso/Examples.lean +++ b/src/examples/SubVerso/Examples.lean @@ -169,7 +169,7 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example "ELAN_TOOLCHAIN", "DYLD_LIBRARY_PATH", "LD_LIBRARY_PATH"] let cmd := "elan" - let args := #["run", toolchain, "lake", "build", ":examples"] + let args := #["run", "--install", toolchain, "lake", "build", ":examples"] -- Build the facet let res ← IO.Process.output { From bd89103404390813674807f52c3cf7feb1cb0389 Mon Sep 17 00:00:00 2001 From: Joachim Breitner Date: Wed, 17 Apr 2024 14:32:07 +0200 Subject: [PATCH 4/4] .trim --- src/examples/SubVerso/Examples.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/examples/SubVerso/Examples.lean b/src/examples/SubVerso/Examples.lean index 74dc74c..5cd2acb 100644 --- a/src/examples/SubVerso/Examples.lean +++ b/src/examples/SubVerso/Examples.lean @@ -158,7 +158,7 @@ partial def loadExamples (leanProject : FilePath) : IO (NameMap (NameMap Example let toolchainfile := projectDir / "lean-toolchain" if !(← toolchainfile.pathExists) then throw <| .userError s!"File {toolchainfile} doesn't exist, couldn't load project" - let toolchain := ← IO.FS.readFile toolchainfile + let toolchain := (← IO.FS.readFile toolchainfile).trim -- 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