feat: lake: detect Elan install and Elan toolchain

This commit is contained in:
tydeu 2023-09-08 19:08:20 -04:00 committed by Mac Malone
parent 7b9d8a04c2
commit becc6fdb0e
6 changed files with 161 additions and 63 deletions

View file

@ -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

View file

@ -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

View file

@ -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),

View file

@ -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 `<lean-sysroot>/lib/lean`, and its system libraries in
`<lean-sysroot>/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 `<home>/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 `<lake-home>/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 `<sysroot>/bin`,
their Lean libraries in `<sysroot>/lib/lean`,
Lean's source files in `<sysroot>/src/lean`,
and Lake's source files in `<sysroot>/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
`<sysroot>/bin`, their Lean libraries in `<sysroot>/lib/lean`, Lean's source files
in `<sysroot>/src/lean`, and Lake's source files in `<sysroot>/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?)

View file

@ -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. -/

View file

@ -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