fix: don't set LEAN_CC unless necessary + detect src dirs
closes leanprover/lake#93
This commit is contained in:
tydeu
parent
9e87958312
commit
df8085b7c2
5 changed files with 97 additions and 41 deletions
|
|
@ -8,23 +8,23 @@ import Lake.Util.NativeLib
|
|||
open System
|
||||
namespace Lake
|
||||
|
||||
/-- Standard path of `lean` in Lean installation. -/
|
||||
/-- Standard path of `lean` in a Lean installation. -/
|
||||
def leanExe (sysroot : FilePath) :=
|
||||
sysroot / "bin" / "lean" |>.withExtension FilePath.exeExtension
|
||||
|
||||
/-- Standard path of `leanc` in Lean installation. -/
|
||||
/-- Standard path of `leanc` in a Lean installation. -/
|
||||
def leancExe (sysroot : FilePath) :=
|
||||
sysroot / "bin" / "leanc" |>.withExtension FilePath.exeExtension
|
||||
|
||||
/-- Standard path of `llvm-ar` in Lean installation. -/
|
||||
/-- Standard path of `llvm-ar` in a Lean installation. -/
|
||||
def leanArExe (sysroot : FilePath) :=
|
||||
sysroot / "bin" / "llvm-ar" |>.withExtension FilePath.exeExtension
|
||||
|
||||
/-- Standard path of `clang` in Lean installation. -/
|
||||
/-- Standard path of `clang` in a Lean installation. -/
|
||||
def leanCcExe (sysroot : FilePath) :=
|
||||
sysroot / "bin" / "clang" |>.withExtension FilePath.exeExtension
|
||||
|
||||
/-- Standard path of `libleanshared` in Lean installation. -/
|
||||
/-- Standard path of `libleanshared` in a Lean installation. -/
|
||||
def leanSharedLib (sysroot : FilePath) :=
|
||||
let dir :=
|
||||
if Platform.isWindows then
|
||||
|
|
@ -37,21 +37,28 @@ def leanSharedLib (sysroot : FilePath) :=
|
|||
structure LeanInstall where
|
||||
sysroot : FilePath
|
||||
githash : String
|
||||
libDir := sysroot / "lib"
|
||||
srcDir := sysroot / "src" / "lean"
|
||||
oleanDir := sysroot / "lib" / "lean"
|
||||
includeDir := sysroot / "include"
|
||||
libDir := sysroot / "lib"
|
||||
lean := leanExe sysroot
|
||||
leanc := leancExe sysroot
|
||||
sharedLib := leanSharedLib sysroot
|
||||
ar : FilePath
|
||||
cc : FilePath
|
||||
customCc : Bool
|
||||
deriving Inhabited, Repr
|
||||
|
||||
/-- Standard path of `lake` in a Lake installation. -/
|
||||
def lakeExe (buildHome : FilePath) :=
|
||||
buildHome / "bin" / "lake" |>.withExtension FilePath.exeExtension
|
||||
|
||||
/-- Path information about the local Lake installation. -/
|
||||
structure LakeInstall where
|
||||
home : FilePath
|
||||
oleanDir := home / "lib"
|
||||
lake := home / "bin" / "lake" |>.withExtension FilePath.exeExtension
|
||||
srcDir := home
|
||||
oleanDir := home / "build" / "lib"
|
||||
lake := lakeExe <| home / "build"
|
||||
deriving Inhabited, Repr
|
||||
|
||||
/--
|
||||
|
|
@ -76,7 +83,7 @@ Construct the `LeanInstall` object for the given Lean sysroot.
|
|||
|
||||
Does two things:
|
||||
1. Invokes `lean` to find out its `githash`.
|
||||
2. Finds the default `ar` and `cc` to use with Lean.
|
||||
2. Finds the `ar` and `cc` to use with Lean.
|
||||
|
||||
For (1), if the invocation fails, `githash` is set to the empty string.
|
||||
|
||||
|
|
@ -85,13 +92,18 @@ Otherwise, if Lean is packaged with an `llvm-ar` and/or `clang`, use them.
|
|||
If not, use the `ar` and/or `cc` in the system's `PATH`. This last step is
|
||||
needed because internal builds of Lean do not bundle these tools
|
||||
(unlike user-facing releases).
|
||||
We also track whether `LEAN_CC` was set to determine whether it should
|
||||
be set in the future for `lake env`. This is because if `LEAN_CC` was not set,
|
||||
it needs to remain not set for `leanc` to work (even setting it to the bundled
|
||||
compiler will break it -- see https://github.com/leanprover/lean4/issues/1281).
|
||||
-/
|
||||
def LeanInstall.get (sysroot : FilePath) : BaseIO LeanInstall := do
|
||||
let (cc, customCc) ← findCc
|
||||
return {
|
||||
sysroot,
|
||||
githash := ← getGithash
|
||||
ar := ← findAr
|
||||
cc := ← findCc
|
||||
cc, customCc
|
||||
}
|
||||
where
|
||||
getGithash := do
|
||||
|
|
@ -110,10 +122,11 @@ where
|
|||
if (← ar.pathExists) then pure ar else pure "ar"
|
||||
findCc := do
|
||||
if let some cc ← IO.getEnv "LEAN_CC" then
|
||||
return cc
|
||||
return (FilePath.mk cc, true)
|
||||
else
|
||||
let cc := leanCcExe sysroot
|
||||
if (← cc.pathExists) then pure cc else pure "cc"
|
||||
let cc := if (← cc.pathExists) then cc else "cc"
|
||||
return (cc, false)
|
||||
|
||||
/--
|
||||
Try to find the installation of the given `lean` command
|
||||
|
|
@ -140,10 +153,10 @@ def findLakeLeanJointHome? : BaseIO (Option FilePath) := do
|
|||
|
||||
/--
|
||||
Try to get Lake's home by assuming
|
||||
the executable is located at `<lake-home>/bin/lake`.
|
||||
the executable is located at `<lake-home>/build/bin/lake`.
|
||||
-/
|
||||
def lakeBuildHome? (lake : FilePath) : Option FilePath :=
|
||||
lake.parent.bind FilePath.parent
|
||||
def lakePackageHome? (lake : FilePath) : Option FilePath := do
|
||||
(← (← lake.parent).parent).parent
|
||||
|
||||
/--
|
||||
Try to find Lean's installation by
|
||||
|
|
@ -164,17 +177,18 @@ def findLeanInstall? : BaseIO (Option LeanInstall) := do
|
|||
/--
|
||||
Try to find Lake's installation by
|
||||
first checking the `LAKE_HOME` environment variable
|
||||
and then by trying the `lakeBuildHome?` of the running executable.
|
||||
and then by trying the `lakePackageHome?` of the running executable.
|
||||
|
||||
It assumes that the Lake installation is setup the same way it is built.
|
||||
That is, with its binary located at `<lake-home>/bin/lake` and its static
|
||||
library and `.olean` files in `<lake-home>/lib`.
|
||||
That is, with its binary located at `<lake-home>/build/bin/lake` and its static
|
||||
library and `.olean` files in `<lake-home>/build/lib`, and its source files
|
||||
located directly in `<lake-home>`.
|
||||
-/
|
||||
def findLakeInstall? : BaseIO (Option LakeInstall) := do
|
||||
if let some home ← IO.getEnv "LAKE_HOME" then
|
||||
return some {home}
|
||||
if let Except.ok lake ← IO.appPath.toBaseIO then
|
||||
if let some home := lakeBuildHome? lake then
|
||||
if let some home := lakePackageHome? lake then
|
||||
return some {home, lake}
|
||||
return none
|
||||
|
||||
|
|
@ -184,15 +198,24 @@ 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/lean`.
|
||||
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`.
|
||||
-/
|
||||
def findInstall? : BaseIO (Option LeanInstall × Option LakeInstall) := do
|
||||
if let some home ← findLakeLeanJointHome? then
|
||||
let lean ← LeanInstall.get home
|
||||
return (
|
||||
some <| ← LeanInstall.get home,
|
||||
some {home, oleanDir := home / "lib" / "lean"}
|
||||
some lean,
|
||||
some {
|
||||
home,
|
||||
srcDir := lean.srcDir / "lake",
|
||||
oleanDir := lean.oleanDir,
|
||||
lake := lakeExe lean.sysroot
|
||||
}
|
||||
)
|
||||
else
|
||||
return (← findLeanInstall?, ← findLakeInstall?)
|
||||
|
|
|
|||
|
|
@ -45,6 +45,8 @@ instance [MonadLake m] [Monad m] [MonadLiftT n m] : MonadLiftT (LakeT n) m where
|
|||
section
|
||||
variable [MonadLake m] [Functor m]
|
||||
|
||||
/- ## Workspace Helpers -/
|
||||
|
||||
@[inline] def findPackage? (name : Name) : m (Option Package) :=
|
||||
(·.findPackage? name) <$> getWorkspace
|
||||
|
||||
|
|
@ -69,11 +71,13 @@ variable [MonadLake m] [Functor m]
|
|||
@[inline] def getLibPath : m SearchPath :=
|
||||
(·.libPath) <$> getWorkspace
|
||||
|
||||
/- ## Lean Install Helpers -/
|
||||
|
||||
@[inline] def getLeanSysroot : m FilePath :=
|
||||
(·.sysroot) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLeanLibDir : m FilePath :=
|
||||
(·.libDir) <$> getLeanInstall
|
||||
@[inline] def getLeanSrcDir : m FilePath :=
|
||||
(·.srcDir) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLeanOleanDir : m FilePath :=
|
||||
(·.oleanDir) <$> getLeanInstall
|
||||
|
|
@ -81,45 +85,74 @@ variable [MonadLake m] [Functor m]
|
|||
@[inline] def getLeanIncludeDir : m FilePath :=
|
||||
(·.includeDir) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLeanLibDir : m FilePath :=
|
||||
(·.libDir) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLean : m FilePath :=
|
||||
(·.lean) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLeanc : m FilePath :=
|
||||
(·.leanc) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLeanSharedLib : m FilePath :=
|
||||
(·.sharedLib) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLeanAr : m FilePath :=
|
||||
(·.ar) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLeanCc : m FilePath :=
|
||||
(·.cc) <$> getLeanInstall
|
||||
|
||||
@[inline] def getLake : m FilePath :=
|
||||
(·.lake) <$> getLakeInstall
|
||||
@[inline] def getLeanCc? : m (Option String) :=
|
||||
(fun lean => if lean.customCc then lean.cc.toString else none) <$> getLeanInstall
|
||||
|
||||
/- ## Lake Install Helpers -/
|
||||
|
||||
@[inline] def getLakeHome : m FilePath :=
|
||||
(·.home) <$> getLakeInstall
|
||||
|
||||
@[inline] def getLakeSrcDir : m FilePath :=
|
||||
(·.srcDir) <$> getLakeInstall
|
||||
|
||||
@[inline] def getLakeOleanDir : m FilePath :=
|
||||
(·.oleanDir) <$> getLakeInstall
|
||||
|
||||
@[inline] def getLake : m FilePath :=
|
||||
(·.lake) <$> getLakeInstall
|
||||
|
||||
end
|
||||
|
||||
@[inline] def getAugmentedLeanPath : LakeT IO SearchPath := do
|
||||
return (← getSearchPath "LEAN_PATH") ++ (← getLeanPath)
|
||||
/--
|
||||
Get `LEAN_PATH` augmented with the workspace's `leanPath` and Lake's `oleanDir`.
|
||||
|
||||
@[inline] def getAugmentedLeanSrcPath : LakeT IO SearchPath := do
|
||||
return (← getSearchPath "LEAN_SRC_PATH") ++ (← getLeanSrcPath)
|
||||
Including Lake's `oleanDir` at the end ensures that same Lake package being
|
||||
used to build is available to the environment (and thus, e.g., the Lean server).
|
||||
Otherwise, it may fall back on whatever the default Lake instance is.
|
||||
-/
|
||||
@[inline] def getAugmentedLeanPath : LakeT BaseIO SearchPath := do
|
||||
return (← getSearchPath "LEAN_PATH") ++ (← getLeanPath) ++ [← getLakeOleanDir]
|
||||
|
||||
@[inline] def getAugmentedLibPath : LakeT IO SearchPath := do
|
||||
/--
|
||||
Get `LEAN_SRC_PATH` augmented with the workspace's `leanSrcPath` and Lake's `srcDir`.
|
||||
|
||||
Including Lake's `srcDir` at the end ensures that same Lake package being
|
||||
used to build is available to the environment (and thus, e.g., the Lean server).
|
||||
Otherwise, it may fall back on whatever the default Lake instance is.
|
||||
-/
|
||||
@[inline] def getAugmentedLeanSrcPath : LakeT BaseIO SearchPath := do
|
||||
return (← getSearchPath "LEAN_SRC_PATH") ++ (← getLeanSrcPath) ++ [← getLakeSrcDir]
|
||||
|
||||
/- Get `sharedLibPathEnv` augmented with the workspace's `libPath`. -/
|
||||
@[inline] def getAugmentedLibPath : LakeT BaseIO SearchPath := do
|
||||
return (← getSearchPath sharedLibPathEnvVar) ++ (← getLibPath)
|
||||
|
||||
def getAugmentedEnv : LakeT IO (Array (String × Option String)) :=
|
||||
def getAugmentedEnv : LakeT BaseIO (Array (String × Option String)) :=
|
||||
return #[
|
||||
("LAKE", (← getLake).toString),
|
||||
("LAKE_HOME", (← getLakeHome).toString),
|
||||
("LEAN_SYSROOT", (← getLeanSysroot).toString),
|
||||
("LEAN_AR", (← getLeanAr).toString),
|
||||
("LEAN_CC", (← getLeanCc).toString),
|
||||
("LEAN_CC", ← getLeanCc?),
|
||||
("LEAN_PATH", (← getAugmentedLeanPath).toString),
|
||||
("LEAN_SRC_PATH", (← getAugmentedLeanSrcPath).toString),
|
||||
(sharedLibPathEnvVar, (← getAugmentedLibPath).toString)
|
||||
|
|
|
|||
|
|
@ -15,7 +15,7 @@ uses when interpreting package configuration files.
|
|||
|
||||
In order to use the Lean stdlib (e.g., `Init`),
|
||||
the executable needs the search path to include the directory
|
||||
with the stdlib's `.olean` files (e.g., from `<lean-home>/lib/lean`).
|
||||
with the stdlib's `.olean` files (e.g., from `<lean-sysroot>/lib/lean`).
|
||||
In order to use Lake's modules as well, the search path also
|
||||
needs to include Lake's `.olean` files (e.g., from `build`).
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
/-
|
||||
Copyright (c) 2021 Mac Malone. All rights reserved.
|
||||
Copyright (c) 2022 Mac Malone. All rights reserved.
|
||||
Released under Apache 2.0 license as described in the file LICENSE.
|
||||
Authors: Mac Malone
|
||||
-/
|
||||
|
|
@ -36,7 +36,7 @@ def sharedLibPathEnvVar :=
|
|||
"LD_LIBRARY_PATH"
|
||||
|
||||
/-- Gets a `SearchPath` from an environment variable. -/
|
||||
def getSearchPath (envVar : String) : IO SearchPath := do
|
||||
def getSearchPath (envVar : String) : BaseIO SearchPath := do
|
||||
match (← IO.getEnv envVar) with
|
||||
| some path => pure <| SearchPath.parse path
|
||||
| none => pure []
|
||||
|
|
|
|||
|
|
@ -293,8 +293,8 @@ Thank Anders Christiansen Sørby ([@Anderssorby](https://github.com/Anderssorby)
|
|||
|
||||
### Augmenting Lake's Search Path
|
||||
|
||||
The `lake` executable needs to know where to find the `.olean` files for the modules used in the package configuration file. Lake will intelligently setup an initial search path based on the location of its own executable and `lean`.
|
||||
The `lake` executable needs to know where to find the Lean library files (e.g., `.olean`. `.ilean`) for the modules used in the package configuration file (and their source files for go-to-definition support in the editor). Lake will intelligently setup an initial search path based on the location of its own executable and `lean`.
|
||||
|
||||
Specifically, 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 `.olean` files at `<lean-home/lib/lean`. 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>/lib`.
|
||||
Specifically, 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 under 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`. Otherwise, it will run `lean --print-prefix` to find Lean's sysroot and assume that Lean's files are located as aforementioned, but that `lake` is at `<lake-home>/build/bin/lake` with its Lean libraries at `<lake-home>/build/lib` and its sources in directly in `<lake-home>`.
|
||||
|
||||
This search path can be augmented by including other directories of `.olean` files in the `LEAN_PATH` environment variable, allowing the user to correct Lake's search if the `.olean` files for Lean (or Lake itself) are in non-standard locations. However, such directories will *not* take precedence over the initial search path. This is important in development, as it prevents the Lake version being used to build Lake from using the Lake version being built's `.olean` files to elaborate Lake's `lakefile.lean` (which can lead to all kinds of errors).
|
||||
This search path can be augmented by including other directories of Lean libraries in the `LEAN_PATH` environment variable (and their sources in `LEAN_SRC_PATH`), allowing the user to correct Lake's search if the files for Lean (or Lake itself) are in non-standard locations. However, such directories will *not* take precedence over the initial search path. This is important in development, as it prevents the Lake version being used to build Lake from using the Lake version being built's Lean libraries to elaborate Lake's `lakefile.lean` (which can lead to all kinds of errors).
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue