refactor: replace leanpkg.toml with a lakefile.lean + build reorg

Lake/InstallPath.lean

@@ -22,7 +22,7 @@ structure LakeInstall where
   home : FilePath
   binDir := home / "bin"
   libDir := home / "lib"
-  oleanDir := home
+  oleanDir := libDir
   lake := binDir / "lake"
   deriving Inhabited, Repr
 
@@ -93,14 +93,14 @@ def findLeanInstall? : IO (Option LeanInstall) := do
   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 at `<lake-home>/bin/lake`, its static library
-  in `<lake-home>/lib` and its `.olean` files directly in `<lake-home>`.
+  That is, with its binary located at `<lake-home>/bin/lake` and its static
+  library and `.olean` files in `<lake-home>/lib`.
 -/
 def findLakeInstall? : IO (Option LakeInstall) := do
   if let some home ← IO.getEnv "LAKE_HOME" then
-    return some {home, oleanDir  := home}
+    return some {home}
   if let some home ← findLakeBuildHome? then
-    return some  {home, oleanDir  := home}
+    return some {home}
   return none
 
 /--
@@ -115,7 +115,6 @@ def findLakeInstall? : IO (Option LakeInstall) := do
 -/
 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})
+    return (some {home}, some {home, libDir := home / "lib" / "lake"})
   else
     return (← findLeanInstall?, ← findLakeInstall?)

README.md

@@ -5,13 +5,15 @@ With Lake, package configuration is written in Lean inside a dedicated `lakefile
 
 ## Building and Running Lake
 
-As Lake functions as an alternative to `leanpkg`, it is not built with it. Instead, there is a pre-packaged `build.sh` shell script which is used to build Lake. It passes it arguments down to a `make` command. So, if you have more than one core, you will probably want to use a `-jX` option to specify how many build tasks you want it to run in parallel. For example:
+If you already have a Lean installation with `lake` packaged with it, you can build a new `lake` by just running `lake build`.
+
+Otherwise, there is a pre-packaged `build.sh` shell script that can be used to build Lake. It passes it arguments down to a `make` command. So, if you have more than one core, you will probably want to use a `-jX` option to specify how many build tasks you want it to run in parallel. For example:
 
 ```shell
 $ ./build.sh -j4
 ```
 
-After building, the `lake` binary will be located at `build/bin/lake` and the library's `.olean` files will be located directly in `build`.
+After building, the `lake` binary will be located at `build/bin/lake` and the library's `.olean` files will be located in `build/lib`.
 
 ### Building with Nix Flakes
 

build.sh

@@ -4,4 +4,4 @@ if [ "$OS" = "Windows_NT" ]; then
 else
   LINK_OPTS=-rdynamic
 fi
-leanmake PKG=Lake BIN_NAME=lake LEAN_PATH=./build bin LINK_OPTS=${LINK_OPTS} "$@"
+leanmake PKG=Lake OLEAN_OUT=build/lib TEMP_OUT=build/ir BIN_NAME=lake LEAN_PATH=./build bin LINK_OPTS=${LINK_OPTS} "$@"

examples/bootstrap/lakefile.lean

@@ -3,7 +3,6 @@ open System Lake DSL
 
 package lake where
   srcDir := FilePath.mk ".." / ".."
-  oleanDir := "."
   binRoot := `Lake.Main
   moreLinkArgs :=
     if Platform.isWindows then

lakefile.lean

@@ -0,0 +1,10 @@
+import Lake
+open System Lake DSL
+
+package lake where
+  binRoot := `Lake.Main
+  moreLinkArgs :=
+    if Platform.isWindows then
+      #["-Wl,--export-all"]
+    else
+      #["-rdynamic"]

lean-toolchain

@@ -0,0 +1 @@
+leanprover/lean4:nightly-2021-10-16

leanpkg.toml

@@ -1,4 +0,0 @@
-[package]
-name = "lake"
-version = "3.0.0-pre"
-lean_version = "leanprover/lean4:nightly-2021-10-09"