From 3bcd18a1c6cae071efe1365249a4402975f76a2f Mon Sep 17 00:00:00 2001 From: tydeu Date: Tue, 5 Oct 2021 20:00:30 -0400 Subject: [PATCH] refactor: generalize Lean/Lake installation detection --- Lake.lean | 2 + Lake/Cli.lean | 67 +++++++++++++++++++------- Lake/InstallPath.lean | 109 ++++++++++++++++++++++++++++++++++++++++++ Lake/LeanVersion.lean | 12 ----- Lake/Main.lean | 1 - Lake/SearchPath.lean | 72 ++++++---------------------- 6 files changed, 177 insertions(+), 86 deletions(-) create mode 100644 Lake/InstallPath.lean diff --git a/Lake.lean b/Lake.lean index d30c8eb713..828fe72986 100644 --- a/Lake.lean +++ b/Lake.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lake.Async +import Lake.Attributes import Lake.BuildBin import Lake.BuildModule import Lake.BuildMonad @@ -19,6 +20,7 @@ import Lake.Git import Lake.Glob import Lake.Help import Lake.Init +import Lake.InstallPath import Lake.LeanConfig import Lake.LeanVersion import Lake.Package diff --git a/Lake/Cli.lean b/Lake/Cli.lean index bfe38198ce..c46b40ba60 100644 --- a/Lake/Cli.lean +++ b/Lake/Cli.lean @@ -7,6 +7,8 @@ import Lake.Init import Lake.Help import Lake.BuildBin import Lake.LeanConfig +import Lake.SearchPath +import Lake.InstallPath import Lake.CliT open System @@ -29,8 +31,10 @@ def Package.clean (self : Package) : IO PUnit := do structure CliOptions where wantsHelp : Bool := false dir : FilePath := "." - file : FilePath := defaultConfigFile + configFile : FilePath := defaultConfigFile subArgs : List String := [] + leanInstall? : Option LeanInstall := none + lakeInstall? : Option LakeInstall := none abbrev CliM := CliT <| StateT CliOptions IO @@ -40,31 +44,39 @@ open CliT -- ## State Management def getDir : CliM FilePath := - getThe CliOptions >>= (·.dir) + CliOptions.dir <$> getThe CliOptions def setDir (dir : FilePath) : CliM PUnit := modifyThe CliOptions fun st => {st with dir := dir} -def getFile : CliM FilePath := - getThe CliOptions >>= (·.file) +def getConfigFile : CliM FilePath := + CliOptions.configFile <$> getThe CliOptions -def setFile (file : FilePath) : CliM PUnit := - modifyThe CliOptions fun st => {st with file := file} +def setConfigFile (file : FilePath) : CliM PUnit := + modifyThe CliOptions fun st => {st with configFile := file} def getSubArgs : CliM (List String) := - getThe CliOptions >>= (·.subArgs) + CliOptions.subArgs <$> getThe CliOptions def setSubArgs (args : List String) : CliM PUnit := modifyThe CliOptions fun st => {st with subArgs := args} def getWantsHelp : CliM Bool := - getThe CliOptions >>= (·.wantsHelp) + CliOptions.wantsHelp <$> getThe CliOptions def setWantsHelp : CliM PUnit := modifyThe CliOptions fun st => {st with wantsHelp := true} +def getLeanInstall? : CliM (Option LeanInstall) := + CliOptions.leanInstall? <$> getThe CliOptions + +def getLakeInstall? : CliM (Option LakeInstall) := + CliOptions.lakeInstall? <$> getThe CliOptions + def loadPkg (args : List String) : CliM Package := do - let dir ← getDir; let file ← getFile; Package.load dir args (dir / file) + let dir ← getDir; let file ← getConfigFile + setupLeanSearchPath (← getLeanInstall?) (← getLakeInstall?) + Package.load dir args (dir / file) def takeArg : CliM String := do match (← takeArg?) with @@ -84,7 +96,7 @@ def unknownShortOption (opt : Char) : CliM PUnit := def shortOption : (opt : Char) → CliM PUnit | 'h' => setWantsHelp | 'd' => do setDir (← takeFileArg) -| 'f' => do setFile (← takeFileArg) +| 'f' => do setConfigFile (← takeFileArg) | opt => unknownShortOption opt def unknownLongOption (opt : String) : CliM PUnit := @@ -93,7 +105,7 @@ def unknownLongOption (opt : String) : CliM PUnit := def longOption : (opt : String) → CliM PUnit | "--help" => setWantsHelp | "--dir" => do setDir (← takeFileArg) -| "--file" => do setFile (← takeFileArg) +| "--file" => do setConfigFile (← takeFileArg) | "--" => do setSubArgs (← takeArgs) | opt => unknownLongOption opt @@ -127,6 +139,27 @@ def noArgsRem (act : CliM UInt32) : CliM UInt32 := do if args.isEmpty then act else error s!"unexpected arguments: {" ".intercalate args}" +def verifyLeanVersion : CliM UInt32 := do + if let some leanInstall ← getLeanInstall? then + let out ← IO.Process.output { + cmd := leanInstall.lean.toString, + args := #["--version"] + } + if out.exitCode == 0 then + if out.stdout.drop 14 |>.startsWith uiLeanVersionString then + pure 0 + else + error s!"expected {uiLeanVersionString}, but got {out.stdout.trim}" + else + error s!"running `lean --version` exited with code {out.exitCode}" + else + error "no lean installation detected" + +def verifyInstall : CliM UInt32 := do + IO.println s!"Lean:\n{repr <| ← getLeanInstall?}" + IO.println s!"Lake:\n{repr <| ← getLakeInstall?}" + verifyLeanVersion + def command : (cmd : String) → CliM UInt32 | "new" => do noArgsRem <| execIO <| new (← takeArg) | "init" => do noArgsRem <| execIO <| init (← takeArg) @@ -138,7 +171,7 @@ def command : (cmd : String) → CliM UInt32 | "build-bin" => do noArgsRem <| execIO <| buildBin (← loadPkg (← getSubArgs)) | "clean" => do noArgsRem <| execIO <| (← loadPkg (← getSubArgs)).clean | "help" => do output <| help (← takeArg?) -| "self-check" => noArgsRem <| execIO verifyLeanVersion +| "self-check" => noArgsRem <| verifyInstall | cmd => error s!"unknown command '{cmd}'" def processArgs : CliM UInt32 := do @@ -148,15 +181,17 @@ def processArgs : CliM UInt32 := do | _ => -- normal CLI processOptions if let some cmd ← takeArg? then - if (← getWantsHelp) then output (help cmd) else command cmd + if (← getWantsHelp) then output (help cmd) else + command cmd else if (← getWantsHelp) then output usage else error "expected command" -def run (self : CliM α) (args : List String) : IO α := +def run (self : CliM α) (args : List String) : IO α := do + let (leanInstall?, lakeInstall?) ← findInstall? CliT.run self args { shortOption, longOption, - longShortOption := unknownLongOption - } |>.run' {} + longShortOption := unknownLongOption, + } |>.run' {leanInstall?, lakeInstall?} end CliM diff --git a/Lake/InstallPath.lean b/Lake/InstallPath.lean new file mode 100644 index 0000000000..649b701bbe --- /dev/null +++ b/Lake/InstallPath.lean @@ -0,0 +1,109 @@ +/- +Copyright (c) 2021 Mac Malone. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Mac Malone +-/ +open System +namespace Lake + +/-- Path information about the local Lean installation. -/ +structure LeanInstall where + home : FilePath + binDir := home / "bin" + libDir := home / "lib" / "lean" + oleanDir := libDir + includeDir := home / "include" + lean := binDir / "lean" + leanc := binDir / "leanc" + deriving Inhabited, Repr + +/-- Path information about the local Lake installation. -/ +structure LakeInstall where + home : FilePath + binDir := home / "bin" + libDir := home / "lib" + oleanDir := home + lake := binDir / "lake" + deriving Inhabited, Repr + +/-- + Try to find the home of the `Lean` in `PATH` (if one exists) + by calling `lean --print-prefix` and returning the path it prints. +-/ +def findLeanPathHome? : IO (Option FilePath) := do + let out ← IO.Process.output { + cmd := "lean", + args := #["--print-prefix"] + } + if out.exitCode == 0 then + some <| FilePath.mk <| out.stdout.trim + else + none + +/-- + Try to get Lake's home by assuming + this executable is located at `/bin/lake`. +-/ +def findLakeBuildHome? : IO (Option FilePath) := do + (← IO.appPath).parent.bind FilePath.parent + +/-- + Check if Lake's executable is co-located with Lean, and, if so, + try to return their joint home by assuming they are located at `/bin`. +-/ +def findLakeLeanJointHome? : IO (Option FilePath) := do + let appPath ← IO.appPath + if let some appDir := appPath.parent then + let leanExe := appDir / "lean" |>.withExtension FilePath.exeExtension + if (← leanExe.pathExists) then + return appDir.parent + return none + +/-- + Try to find Lean's installation path by + first checking the `LEAN_HOME` environment variable + and then by trying `findLeanPathHome?`. + + It assumes that the Lean installation is setup the normal way. + That is, with its binaries located in `/bin/lake` and its + libraries and `.olean` files located in `/lib/lean`. +-/ +def findLeanInstall? : IO (Option LeanInstall) := do + if let some home ← IO.getEnv "LEAN_HOME" then + return some {home} + if let some home ← findLeanPathHome? then + return some {home} + return none + +/-- + Try to find Lake's installation path by + first checking the `LAKE_HOME` environment variable + and then by trying `findLakeBuildHome?`. + + It assumes that the Lake installation is setup the same way it is built. + That is, with its binary located in `/bin/lake`, its static library + in `/lib` and its `.olean` files directly in ``. +-/ +def findLakeInstall? : IO (Option LakeInstall) := do + if let some home ← IO.getEnv "LAKE_HOME" then + return some {home, oleanDir := home} + if let some home ← findLakeBuildHome? then + return some {home, oleanDir := home} + return none + +/-- + Try to get Lake's install path by first trying `findLakeLeanHome?` + then by running `findLeanInstall?` and `findLakeInstall?`. + + 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 their binaries are located in `/bin` with + Lean's libraries and `.olean` files at `/lib/lean` and + Lake's static library and `.olean` files at `/lib/lake`. +-/ +def findInstall? : IO (Option LeanInstall × Option LakeInstall) := do + if let some home ← findLakeLeanJointHome? then + let libDir := home / "lib" / "lake" + return (some {home}, some {home, libDir, oleanDir := libDir}) + else + return (← findLeanInstall?, ← findLakeInstall?) diff --git a/Lake/LeanVersion.lean b/Lake/LeanVersion.lean index de5633a10b..99c8b7f62d 100644 --- a/Lake/LeanVersion.lean +++ b/Lake/LeanVersion.lean @@ -25,15 +25,3 @@ else if Lean.version.specialDesc ≠ "" then s!"{leanVersionStringCore}-{Lean.version.specialDesc}" else s!"master ({leanVersionStringCore})" - -def verifyLeanVersion : IO PUnit := do - let out ← IO.Process.output { - cmd := "lean", - args := #["--version"] - } - if out.exitCode == 0 then - unless out.stdout.drop 14 |>.startsWith uiLeanVersionString do - throw <| IO.userError <| - s!"expected {uiLeanVersionString}, but got {out.stdout.trim}" - else - throw <| IO.userError <| "missing lean!" diff --git a/Lake/Main.lean b/Lake/Main.lean index 40b9f1dadc..30779fdf04 100644 --- a/Lake/Main.lean +++ b/Lake/Main.lean @@ -6,5 +6,4 @@ Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone import Lake def main (args : List String) : IO UInt32 := do - Lake.setupLeanSearchPath Lake.cli args -- should not throw errors (outside user code) diff --git a/Lake/SearchPath.lean b/Lake/SearchPath.lean index b3d6070675..93e1a7b806 100644 --- a/Lake/SearchPath.lean +++ b/Lake/SearchPath.lean @@ -4,44 +4,11 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Mac Malone -/ import Lean.Util.Path +import Lake.InstallPath open System namespace Lake -/-- - Try to find the home of Lean by calling - `lean --print-prefix` and returning the path it prints. --/ -def getLeanHome? : IO (Option FilePath) := do - let out ← IO.Process.output { - cmd := "lean", - args := #["--print-prefix"] - } - if out.exitCode == 0 then - some <| FilePath.mk <| out.stdout.trim - else - none - -/-- - Try to get Lake's home by assuming - this executable is located at `/bin/lake`. --/ -def getLakeHome? : IO (Option FilePath) := do - (← IO.appPath).parent.bind FilePath.parent - - -/-- - Check if Lake's executable is co-located with Lean, and, if so, - try to return their joint home by assuming they are located at `/bin`. --/ -def getAppHome? : IO (Option FilePath) := do - let appPath ← IO.appPath - if let some appDir := appPath.parent then - let leanExe := appDir / "lean" |>.withExtension FilePath.exeExtension - if (← leanExe.pathExists) then - return appDir.parent - return none - /-- Initializes the search path the Lake executable uses when interpreting package configuration files. @@ -53,31 +20,22 @@ def getAppHome? : IO (Option FilePath) := do needs to include Lake's `.olean` files (e.g., from `build`). While this can be done by having the user augment `LEAN_PATH` with - the necessary directories, Lake also intelligently derives an initial - search path from the location of the `lean` executable and itself. + the necessary directories, Lake also intelligently augments the initial + search path with the `.olean` directories of the provided Lean and Lake + installations. - 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 Lean and Lake are located in `/bin` with - Lean's `.olean` files at `/lib/lean` and that `lake` - is at `/bin/lake` with its `.olean` files at ``. - If this is correct, the user will not need to augment `LEAN_PATH`. + See `findInstall?` for more information on how Lake determines those + directories. If everything is configured as expected, the user will not + need to augment `LEAN_PATH`. Otherwise, they will need to provide Lake + with more information (either through `LEAN_PATH` or through other options). -/ -def setupLeanSearchPath : IO Unit := do +def setupLeanSearchPath +(leanInstall? : Option LeanInstall) (lakeInstall? : Option LakeInstall) +: IO Unit := do let mut sp : SearchPath := [] - if let some appHome ← getAppHome? then - -- we are co-located with Lean - let libDir := appHome / "lib" - sp := libDir / "lean" :: libDir / "lake" :: sp - else - -- we are a custom installation - if let some lakeHome ← getLakeHome? then - sp := lakeHome :: sp - if let some leanHome ← getLeanHome? then - sp := leanHome / "lib" / "lean" :: sp + if let some leanInstall ← leanInstall? then + sp := leanInstall.oleanDir :: sp + if let some lakeInstall ← lakeInstall? then + sp := lakeInstall.oleanDir :: sp sp ← Lean.addSearchPathFromEnv sp Lean.searchPathRef.set sp