46769b64c9
This PR adds a `bootstrap` option to Lake which is used to identify the
core Lean package. This enables Lake to use the current stage's include
directory rather than the Lean toolchains when compiling Lean with Lean
in core.
**Breaking change:** The Lean library directory is no longer part of
`getLeanLinkSharedFlags`. FFI users should provide this option
separately when linking to Lean (e.g.. via `s!"-L{(←
getLeanLibDir).toString}"`). See the FFI example for a demonstration.
59 lines
2.1 KiB
Text
59 lines
2.1 KiB
Text
/-
|
|
Copyright (c) 2021 Sebastian Ullrich. All rights reserved.
|
|
Released under Apache 2.0 license as described in the file LICENSE.
|
|
Authors: Sebastian Ullrich
|
|
-/
|
|
prelude
|
|
import Init.Data.Array.Basic
|
|
import Init.System.FilePath
|
|
|
|
open System
|
|
|
|
namespace Lean.Compiler.FFI
|
|
|
|
@[extern "lean_get_leanc_extra_flags"]
|
|
private opaque getLeancExtraFlags : Unit → String
|
|
|
|
private def flagsStringToArray (s : String) : Array String :=
|
|
s.splitOn.toArray |>.filter (· ≠ "")
|
|
|
|
/--
|
|
Return C compiler flags for including Lean's headers.
|
|
Unlike `getCFlags`, this does not contain the Lean include directory.
|
|
-/
|
|
def getCFlags' : Array String :=
|
|
flagsStringToArray (getLeancExtraFlags ())
|
|
|
|
/-- Return C compiler flags for including Lean's headers. -/
|
|
def getCFlags (leanSysroot : FilePath) : Array String :=
|
|
#["-I", (leanSysroot / "include").toString] ++ getCFlags'
|
|
|
|
@[extern "lean_get_leanc_internal_flags"]
|
|
private opaque getLeancInternalFlags : Unit → String
|
|
|
|
/-- Return C compiler flags needed to use the C compiler bundled with the Lean toolchain. -/
|
|
def getInternalCFlags (leanSysroot : FilePath) : Array String :=
|
|
flagsStringToArray (getLeancInternalFlags ()) |>.map (·.replace "ROOT" leanSysroot.toString)
|
|
|
|
@[extern "lean_get_linker_flags"]
|
|
private opaque getBuiltinLinkerFlags (linkStatic : Bool) : String
|
|
|
|
/--
|
|
Return linker flags for linking against Lean's libraries.
|
|
Unlike `getLinkerFlags`, this does not contain the Lean library directory.
|
|
-/
|
|
def getLinkerFlags' (linkStatic := true) : Array String :=
|
|
flagsStringToArray (getBuiltinLinkerFlags linkStatic)
|
|
|
|
/-- Return linker flags for linking against Lean's libraries. -/
|
|
def getLinkerFlags (leanSysroot : FilePath) (linkStatic := true) : Array String :=
|
|
#["-L", (leanSysroot / "lib" / "lean").toString] ++ getLinkerFlags' linkStatic
|
|
|
|
@[extern "lean_get_internal_linker_flags"]
|
|
private opaque getBuiltinInternalLinkerFlags : Unit → String
|
|
|
|
/-- Return linker flags needed to use the linker bundled with the Lean toolchain. -/
|
|
def getInternalLinkerFlags (leanSysroot : FilePath) : Array String :=
|
|
flagsStringToArray (getBuiltinInternalLinkerFlags ()) |>.map (·.replace "ROOT" leanSysroot.toString)
|
|
|
|
end Lean.Compiler.FFI
|