diff --git a/src/lake/Lake/CLI/Init.lean b/src/lake/Lake/CLI/Init.lean index 4b082fcdda..580bd1d219 100644 --- a/src/lake/Lake/CLI/Init.lean +++ b/src/lake/Lake/CLI/Init.lean @@ -135,7 +135,7 @@ where escape s := Lean.idBeginEscape.toString ++ s ++ Lean.idEndEscape.toString /-- Initialize a new Lake package in the given directory with the given name. -/ -def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit := do +def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) (env : Lake.Env) : LogIO PUnit := do let pkgName := stringToLegalOrSimpleName name -- determine the name to use for the root @@ -172,12 +172,25 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit unless (← mainFile.pathExists) do IO.FS.writeFile mainFile <| mainFileContents rootNameStr - -- write Lean's toolchain to file (if it has one) for `elan` - if Lean.toolchain ≠ "" then + /- + Write the detected toolchain to file (if there is one) for `elan`. + See [lean4#2518][1] for details on the design considerations taken here. + + [1]: https://github.com/leanprover/lean4/issues/2518 + -/ + let toolchainFile := dir / toolchainFileName + if env.toolchain.isEmpty then + -- Empty githash implies dev build + unless env.lean.githash.isEmpty do + unless (← toolchainFile.pathExists) do + logWarning <| + "could not create a `lean-toolchain` file for the new package; " ++ + "no known toolchain name for the current Elan/Lean/Lake" + else if tmp = .math then - download "lean-toolchain" mathToolchainUrl (dir / toolchainFileName) + download "lean-toolchain" mathToolchainUrl toolchainFile else - IO.FS.writeFile (dir / toolchainFileName) <| Lean.toolchain ++ "\n" + IO.FS.writeFile toolchainFile <| env.toolchain ++ "\n" -- update `.gitignore` with additional entries for Lake let h ← IO.FS.Handle.mk (dir / ".gitignore") IO.FS.Mode.append @@ -193,10 +206,10 @@ def initPkg (dir : FilePath) (name : String) (tmp : InitTemplate) : LogIO PUnit else logWarning "failed to initialize git repository" -def init (pkgName : String) (tmp : InitTemplate) : LogIO PUnit := - initPkg "." pkgName tmp +def init (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) : LogIO PUnit := + initPkg "." pkgName tmp env -def new (pkgName : String) (tmp : InitTemplate) : LogIO PUnit := do +def new (pkgName : String) (tmp : InitTemplate) (env : Lake.Env) : LogIO PUnit := do let dirName := pkgName.map fun chr => if chr == '.' then '-' else chr IO.FS.createDir dirName - initPkg dirName pkgName tmp + initPkg dirName pkgName tmp env diff --git a/src/lake/Lake/CLI/Main.lean b/src/lake/Lake/CLI/Main.lean index 8a410fa25b..a1f8f63239 100644 --- a/src/lake/Lake/CLI/Main.lean +++ b/src/lake/Lake/CLI/Main.lean @@ -27,6 +27,7 @@ namespace Lake structure LakeOptions where rootDir : FilePath := "." configFile : FilePath := defaultConfigFile + elanInstall? : Option ElanInstall := none leanInstall? : Option LeanInstall := none lakeInstall? : Option LakeInstall := none configOpts : NameMap String := {} @@ -56,7 +57,7 @@ def LakeOptions.getInstall (opts : LakeOptions) : Except CliError (LeanInstall /-- Compute the Lake environment based on `opts`. Error if an install is missing. -/ def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do - Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall) + Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall) opts.elanInstall? /-- Make a `LoadConfig` from a `LakeOptions`. -/ def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig := @@ -83,8 +84,8 @@ abbrev CliStateM := StateT LakeOptions CliMainM abbrev CliM := ArgsT CliStateM def CliM.run (self : CliM α) (args : List String) : BaseIO ExitCode := do - let (leanInstall?, lakeInstall?) ← findInstall? - let main := self args |>.run' {leanInstall?, lakeInstall?} + let (elanInstall?, leanInstall?, lakeInstall?) ← findInstall? + let main := self args |>.run' {elanInstall?, leanInstall?, lakeInstall?} let main := main.run >>= fun | .ok a => pure a | .error e => error e.toString main.run @@ -176,6 +177,7 @@ def verifyLeanVersion (leanInstall : LeanInstall) : Except CliError PUnit := do /-- Output the detected installs and verify the Lean version. -/ def verifyInstall (opts : LakeOptions) : ExceptT CliError MainM PUnit := do + IO.println s!"Elan:\n{repr <| opts.elanInstall?}" IO.println s!"Lean:\n{repr <| opts.leanInstall?}" IO.println s!"Lake:\n{repr <| opts.lakeInstall?}" let (leanInstall, _) ← opts.getInstall @@ -259,15 +261,17 @@ def scriptCli : (cmd : String) → CliM PUnit protected def new : CliM PUnit := do processOptions lakeOption - let pkgName ← takeArg "package name" - let template ← parseTemplateSpec <| (← takeArg?).getD "" - noArgsRem do MainM.runLogIO (new pkgName template) (← getThe LakeOptions).verbosity + let opts ← getThe LakeOptions + let name ← takeArg "package name" + let tmp ← parseTemplateSpec <| (← takeArg?).getD "" + noArgsRem do MainM.runLogIO (new name tmp (← opts.computeEnv)) opts.verbosity protected def init : CliM PUnit := do processOptions lakeOption - let pkgName ← takeArg "package name" - let template ← parseTemplateSpec <| (← takeArg?).getD "" - noArgsRem do MainM.runLogIO (init pkgName template) (← getThe LakeOptions).verbosity + let opts ← getThe LakeOptions + let name ← takeArg "package name" + let tmp ← parseTemplateSpec <| (← takeArg?).getD "" + noArgsRem do MainM.runLogIO (init name tmp (← opts.computeEnv)) opts.verbosity protected def build : CliM PUnit := do processOptions lakeOption diff --git a/src/lake/Lake/Config/Env.lean b/src/lake/Lake/Config/Env.lean index 09ad13c348..45e84de073 100644 --- a/src/lake/Lake/Config/Env.lean +++ b/src/lake/Lake/Config/Env.lean @@ -22,6 +22,10 @@ structure Env where lake : LakeInstall /-- The Lean installation of the environment. -/ lean : LeanInstall + /-- The Elan installation (if any) of the environment. -/ + elan? : Option ElanInstall + /-- The initial Elan toolchain of the environment (i.e., `ELAN_TOOLCHAIN`). -/ + initToolchain : String /-- The initial Lean library search path of the environment (i.e., `LEAN_PATH`). -/ initLeanPath : SearchPath /-- The initial Lean source search path of the environment (i.e., `LEAN_SRC_PATH`). -/ @@ -35,9 +39,10 @@ structure Env where namespace Env /-- Compute an `Lake.Env` object from the given installs and set environment variables. -/ -def compute (lake : LakeInstall) (lean : LeanInstall) : BaseIO Env := +def compute (lake : LakeInstall) (lean : LeanInstall) (elan? : Option ElanInstall) : BaseIO Env := return { - lake, lean, + lake, lean, elan?, + initToolchain := (← IO.getEnv "ELAN_TOOLCHAIN").getD "" initLeanPath := ← getSearchPath "LEAN_PATH", initLeanSrcPath := ← getSearchPath "LEAN_SRC_PATH", initSharedLibPath := ← getSearchPath sharedLibPathEnvVar, @@ -45,7 +50,17 @@ def compute (lake : LakeInstall) (lean : LeanInstall) : BaseIO Env := } /-- -The Lean library search path of the environment (i.e., `LEAN_PATH`). +The preferred toolchain of the environment. May be empty. +Order is: `env.lean.toolchain` or `env.initToolchain` or 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 + +/-- +The binary search path of the environment (i.e., `PATH`). Combines the initial path of the environment with that of the Lake installation. -/ def path (env : Env) : SearchPath := @@ -83,9 +98,11 @@ Combines the initial path of the environment with that of the Lean installation. def sharedLibPath (env : Env) : SearchPath := env.lean.sharedLibPath ++ env.initSharedLibPath -/-- Environment variable settings based only on the Lean and Lake installations. -/ +/-- Environment variable settings based only on the Elan/Lean/Lake installations. -/ def installVars (env : Env) : Array (String × Option String) := #[ + ("ELAN_HOME", env.elan?.map (·.home.toString)), + ("ELAN_TOOLCHAIN", if env.toolchain.isEmpty then none else env.toolchain), ("LAKE", env.lake.lake.toString), ("LAKE_HOME", env.lake.home.toString), ("LEAN_SYSROOT", env.lean.sysroot.toString), diff --git a/src/lake/Lake/Config/InstallPath.lean b/src/lake/Lake/Config/InstallPath.lean index b0a327788c..1c998e6e87 100644 --- a/src/lake/Lake/Config/InstallPath.lean +++ b/src/lake/Lake/Config/InstallPath.lean @@ -8,6 +8,20 @@ import Lake.Util.NativeLib open System namespace Lake +/-! ## Data Structures -/ + +/-- Standard path of `elan` in a Elan installation. -/ +def elanExe (home : FilePath) := + home / "bin" / "elan" |>.withExtension FilePath.exeExtension + +/-- Information about the local Elan setup. -/ +structure ElanInstall where + home : FilePath + elan := elanExe home + binDir := home / "bin" + toolchainsDir := home / "toolchains" + deriving Inhabited, Repr + /-- Standard path of `lean` in a Lean installation. -/ def leanExe (sysroot : FilePath) := sysroot / "bin" / "lean" |>.withExtension FilePath.exeExtension @@ -37,6 +51,7 @@ def leanSharedLib (sysroot : FilePath) := structure LeanInstall where sysroot : FilePath githash : String + toolchain : String srcDir := sysroot / "src" / "lean" leanLibDir := sysroot / "lib" / "lean" includeDir := sysroot / "include" @@ -77,8 +92,27 @@ structure LakeInstall where lake := lakeExe <| home / "build" deriving Inhabited, Repr +/-- Construct a Lake installation co-located with the specified Lean installation. -/ +def LakeInstall.ofLean (lean : LeanInstall) : LakeInstall where + home := lean.sysroot + srcDir := lean.srcDir / "lake" + binDir := lean.binDir + libDir := lean.leanLibDir + lake := lakeExe lean.sysroot + +/-! ## Detection Functions -/ + /-- -Try to find the sysroot of the given `lean` command (if it exists) +Attempt to detect a Elan installation by checking the `ELAN_HOME` +environment variable for a installation location. +-/ +def findElanInstall? : BaseIO (Option ElanInstall) := do + if let some home ← IO.getEnv "ELAN_HOME" then + return some {home} + return none + +/-- +Attempt to find the sysroot of the given `lean` command (if it exists) by calling `lean --print-prefix` and returning the path it prints. Defaults to trying the `lean` in `PATH`. -/ @@ -98,11 +132,12 @@ def findLeanSysroot? (lean := "lean") : BaseIO (Option FilePath) := do Construct the `LeanInstall` object for the given Lean sysroot. Does the following: -1. Invokes `lean` to find out its `githash`. +1. Invokes `lean` to find out its `githash` and `Lean.toolchain` 2. Finds the `ar` and `cc` to use with Lean. 3. Computes the sub-paths of the Lean install. -For (1), if the invocation fails, `githash` is set to the empty string. +For (1), if the invocation fails, `githash` and `toolchain` are set +to the empty string. For (2), if `LEAN_AR` or `LEAN_CC` are defined, it uses those paths. Otherwise, if Lean is packaged with an `llvm-ar` and/or `clang`, use them. @@ -122,22 +157,30 @@ Lean libraries in `/lib/lean`, and its system libraries in `/lib`. -/ def LeanInstall.get (sysroot : FilePath) : BaseIO LeanInstall := do + let githash ← getGithash + let toolchain ← getToolchain let (cc, customCc) ← findCc - return { - sysroot, - githash := ← getGithash - ar := ← findAr - cc, customCc - } + let ar ← findAr + return {sysroot, githash, toolchain, 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 - let act : IO _ := do + EIO.catchExceptions (h := fun _ => pure "") do let out ← IO.Process.output { cmd := leanExe sysroot |>.toString, args := #["--githash"] } pure <| out.stdout.trim - act.catchExceptions fun _ => pure "" findAr := do if let some ar ← IO.getEnv "LEAN_AR" then return ar @@ -153,7 +196,7 @@ where return (cc, false) /-- -Try to find the installation of the given `lean` command +Attempt to detect the installation of the given `lean` command by calling `findLeanCmdHome?`. See `LeanInstall.get` for how it assumes the Lean install is organized. -/ @@ -161,11 +204,11 @@ def findLeanCmdInstall? (lean := "lean") : BaseIO (Option LeanInstall) := OptionT.run do LeanInstall.get (← findLeanSysroot? lean) /-- -Check if Lake's executable is co-located with Lean, and, if so, +Check if the running Lake's executable is co-located with Lean, and, if so, try to return their joint home by assuming they are both located at `/bin`. -/ def findLakeLeanJointHome? : BaseIO (Option FilePath) := do - if let Except.ok appPath ← IO.appPath.toBaseIO then + if let .ok appPath ← IO.appPath.toBaseIO then if let some appDir := appPath.parent then let leanExe := appDir / "lean" |>.withExtension FilePath.exeExtension if (← leanExe.pathExists) then @@ -173,14 +216,14 @@ def findLakeLeanJointHome? : BaseIO (Option FilePath) := do return none /-- -Try to get Lake's home by assuming +Attempt to detect a specified Lake's executable's home by assuming the executable is located at `/build/bin/lake`. -/ def lakePackageHome? (lake : FilePath) : Option FilePath := do (← (← lake.parent).parent).parent /-- -Try to find Lean's installation by first checking the +Attempt to detect Lean's installation by first checking the `LEAN_SYSROOT` environment variable and then by trying `findLeanCmdHome?`. See `LeanInstall.get` for how it assumes the Lean install is organized. -/ @@ -192,7 +235,7 @@ def findLeanInstall? : BaseIO (Option LeanInstall) := do return none /-- -Try to find Lake's installation by +Attempt to detect Lake's installation by first checking the `LAKE_HOME` environment variable and then by trying the `lakePackageHome?` of the running executable. @@ -210,30 +253,25 @@ def findLakeInstall? : BaseIO (Option LakeInstall) := do return none /-- -Try to get Lake's install path by first trying `findLakeLeanHome?` -then by running `findLeanInstall?` and `findLakeInstall?`. +Attempt to automatically detect an Elan, Lake, and Lean installation. -If Lake is co-located with `lean` (i.e., there is `lean` executable -in the same directory as itself), it will assume it was installed with -Lean and that both Lake's and Lean's files are all located their shared -sysroot. -In particular, their binaries are located in `/bin`, -their Lean libraries in `/lib/lean`, -Lean's source files in `/src/lean`, -and Lake's source files in `/src/lean/lake`. +First, it calls `findElanInstall?` to detect a Elan installation. +Then it attempts to detect if Lake and Lean are part of a single installation +where the `lake` executable is co-located with the `lean` executable (i.e., they +are in the same directory). If Lean and Lake are not co-located, Lake will +attempt to find the their installations separately by calling +`findLeanInstall?` and `findLakeInstall?`. + +When co-located, Lake will assume that Lean and Lake's binaries are located in +`/bin`, their Lean libraries in `/lib/lean`, Lean's source files +in `/src/lean`, and Lake's source files in `/src/lean/lake`, +following the pattern of a regular Lean toolchain. -/ -def findInstall? : BaseIO (Option LeanInstall × Option LakeInstall) := do +def findInstall? : BaseIO (Option ElanInstall × Option LeanInstall × Option LakeInstall) := do + let elan? ← findElanInstall? if let some home ← findLakeLeanJointHome? then let lean ← LeanInstall.get home - return ( - some lean, - some { - home, - srcDir := lean.srcDir / "lake", - binDir := lean.binDir, - libDir := lean.leanLibDir, - lake := lakeExe home - } - ) + let lake := LakeInstall.ofLean lean + return (elan?, lean, lake) else - return (← findLeanInstall?, ← findLakeInstall?) + return (elan?, ← findLeanInstall?, ← findLakeInstall?) diff --git a/src/lake/Lake/Config/Monad.lean b/src/lake/Lake/Config/Monad.lean index e9eb16903c..17a8298dd3 100644 --- a/src/lake/Lake/Config/Monad.lean +++ b/src/lake/Lake/Config/Monad.lean @@ -116,6 +116,10 @@ variable [MonadLakeEnv m] [Functor m] @[inline] def getLakeEnv : m Lake.Env := read +/-- Get the name of Elan toolchain for the Lake environment. Empty if none. -/ +@[inline] def getElanToolchain : m String := + (·.toolchain) <$> getLakeEnv + /-! ### Search Path Helpers -/ /-- Get the detected `LEAN_PATH` value of the Lake environment. -/ @@ -130,6 +134,20 @@ variable [MonadLakeEnv m] [Functor m] @[inline] def getEnvSharedLibPath : m SearchPath := (·.sharedLibPath) <$> getLakeEnv +/-! ### Elan Install Helpers -/ + +/-- Get the detected Elan installation (if one). -/ +@[inline] def getElanInstall? : m (Option ElanInstall) := + (·.elan?) <$> getLakeEnv + +/-- Get the root directory of the detected Elan installation (i.e., `ELAN_HOME`). -/ +@[inline] def getElanHome? : m (Option FilePath) := + (·.map (·.home)) <$> getElanInstall? + +/-- Get the path of the `elan` binary in the detected Elan installation. -/ +@[inline] def getElan? : m (Option FilePath) := + (·.map (·.elan)) <$> getElanInstall? + /-! ### Lean Install Helpers -/ /-- Get the detected Lean installation. -/ diff --git a/src/lake/tests/env/test.sh b/src/lake/tests/env/test.sh index 68ccb66819..700796178e 100755 --- a/src/lake/tests/env/test.sh +++ b/src/lake/tests/env/test.sh @@ -21,9 +21,17 @@ $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 `LEAN_AR=foo $LAKE env printenv LEAN_AR` = foo -test `LEAN_CC=foo $LAKE env printenv LEAN_CC` = foo +test "`LEAN_AR=foo $LAKE env printenv LEAN_AR`" = foo +test "`LEAN_CC=foo $LAKE env printenv LEAN_CC`" = foo # Test that the platform-specific shared library search path is set if [ "$OS" = Windows_NT ]; then