diff --git a/README.md b/README.md index 15f70b5c6f..0c6d1ec75d 100644 --- a/README.md +++ b/README.md @@ -5,21 +5,33 @@ With Lake, package configuration is written in Lean inside a dedicated `package. ## Building and Running Lake -In order to properly build Lake, you must provide `leanpkg build bin` with some additional linker options to have it create an executable that can correctly interpret the Lake package configuration files. +As Lake functions as an alternative to `leanpkg`, the most direct way of building Lake is through `leanmake`. However, you can also build it with `leanpkg`. Either way, you will need to provide some additional linker options to create an executable that can correctly interpret the Lake package configuration files. On Unix: +``` +$ leanmake PKG=Lake LEAN_PATH=./build bin LINK_OPTS=-rdynamic +``` + +or + ``` $ leanpkg build bin LINK_OPTS=-rdynamic ``` On Windows (MSYS2): +``` +$ leanmake PKG=Lake LEAN_PATH=./build bin LINK_OPTS=-Wl,--export-all +``` + +or + ``` $ leanpkg build bin LINK_OPTS=-Wl,--export-all ``` -Alternatively, you can build Lake by running the the pre-packaged `build-msys2.sh` and `build-unix.sh` shell scripts which include these commands. +Alternatively, you can build Lake by running the the pre-packaged `build-msys2.sh` and `build-unix.sh` shell scripts, which include the `leanmake` commands. ### Augmenting Lake's Search Path diff --git a/build-msys2.sh b/build-msys2.sh index 06c3e42b7a..c637e8a3b1 100644 --- a/build-msys2.sh +++ b/build-msys2.sh @@ -1 +1 @@ -leanpkg build bin LINK_OPTS=-Wl,--export-all "$@" +leanmake PKG=Lake LEAN_PATH=./build bin LINK_OPTS=-Wl,--export-all "$@" diff --git a/build-unix.sh b/build-unix.sh index 1d82876db7..ac44230b3a 100644 --- a/build-unix.sh +++ b/build-unix.sh @@ -1 +1 @@ -leanpkg build bin LINK_OPTS=-rdynamic "$@" +leanmake PKG=Lake LEAN_PATH=./build bin LINK_OPTS=-rdynamic "$@"