max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: generalize Lean/Lake installation detection

Browse source
This commit is contained in:
tydeu 2021-10-05 20:00:30 -04:00
parent 4c0734b5f1
commit 3bcd18a1c6
6 changed files with 177 additions and 86 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
Lake.lean
View file

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

67
Lake/Cli.lean
View file

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

109
Lake/InstallPath.lean Normal file
View file

@ -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 `<lake-home>/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 `<home>/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 `<lean-home>/bin/lake` and its
libraries and `.olean` files located in `<lean-home>/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 `<lake-home>/bin/lake`, its static library
in `<lake-home>/lib` and its `.olean` files directly in `<lake-home>`.
-/
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 `<lean-home>/bin` with
Lean's libraries and `.olean` files at `<lean-home>/lib/lean` and
Lake's static library and `.olean` files at `<lean-home>/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?)

12
Lake/LeanVersion.lean
View file

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

1
Lake/Main.lean
View file

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

72
Lake/SearchPath.lean
View file

@ -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 `<lake-home>/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 `<app-home>/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 `<lean-home>/bin` with
Lean's `.olean` files at `<lean-home/lib/lean` and Lake's at `.olean` files
at `<lean-home/lib/lake`.
Otherwise, it will run `lean --print-prefix` to find Lean's home and
assume that its `.olean` files are at `<lean-home>/lib/lean` and that `lake`
is at `<lake-home>/bin/lake` with its `.olean` files at `<lake-home>`.
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