diff --git a/Lake.lean b/Lake.lean index 01b5c45bf3..f6a629bc27 100644 --- a/Lake.lean +++ b/Lake.lean @@ -1,16 +1,29 @@ /- -Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Copyright (c) 2021 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone +Authors: Mac Malone -/ +import Lake.Async +import Lake.BuildBin +import Lake.BuildModule +import Lake.BuildMonad +import Lake.BuildPackage +import Lake.BuildTarget +import Lake.BuildTargets +import Lake.BuildTop import Lake.Cli +import Lake.CliT +import Lake.Compile +import Lake.Git +import Lake.Glob +import Lake.Help +import Lake.Init +import Lake.LeanConfig +import Lake.LeanVersion +import Lake.Package +import Lake.Resolve import Lake.SearchPath - -def main (args : List String) : IO UInt32 := do - try - Lake.setupLeanSearchPath - Lake.cli args - pure 0 - catch e => - IO.eprintln <| "error: " ++ toString e -- avoid "uncaught exception: ..." - pure 1 +import Lake.Target +import Lake.Task +import Lake.Trace +import Lake.Version diff --git a/Lake/Main.lean b/Lake/Main.lean new file mode 100644 index 0000000000..01b5c45bf3 --- /dev/null +++ b/Lake/Main.lean @@ -0,0 +1,16 @@ +/- +Copyright (c) 2017 Microsoft Corporation. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Gabriel Ebner, Sebastian Ullrich, Mac Malone +-/ +import Lake.Cli +import Lake.SearchPath + +def main (args : List String) : IO UInt32 := do + try + Lake.setupLeanSearchPath + Lake.cli args + pure 0 + catch e => + IO.eprintln <| "error: " ++ toString e -- avoid "uncaught exception: ..." + pure 1 diff --git a/examples/bootstrap/package.lean b/examples/bootstrap/package.lean index 4d189efdaf..7d2dc38e83 100644 --- a/examples/bootstrap/package.lean +++ b/examples/bootstrap/package.lean @@ -7,6 +7,7 @@ def package : PackageConfig := { srcDir := FilePath.mk ".." / ".." oleanDir := "." leancArgs := #["-O3", "-DNDEBUG"] + binRoot := `Lake.Main linkArgs := if Platform.isWindows then #["-Wl,--export-all"] diff --git a/examples/bootstrap/package.sh b/examples/bootstrap/package.sh index bd64051f9d..4abc2142f7 100755 --- a/examples/bootstrap/package.sh +++ b/examples/bootstrap/package.sh @@ -1 +1,3 @@ +set -ex +${LAKE:-../../build/bin/lake} build-lib ${LAKE:-../../build/bin/lake} build-bin