max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

refactor: build with leanmake instead of leanpkg

Browse source
This commit is contained in:
tydeu 2021-08-16 09:23:51 -04:00
parent f977ee8b34
commit d49c64453d
3 changed files with 16 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

16
README.md
View file

@ -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

2
build-msys2.sh
View file

@ -1 +1 @@
leanpkg build bin LINK_OPTS=-Wl,--export-all "$@"
leanmake PKG=Lake LEAN_PATH=./build bin LINK_OPTS=-Wl,--export-all "$@"

2
build-unix.sh
View file

@ -1 +1 @@
leanpkg build bin LINK_OPTS=-rdynamic "$@"
leanmake PKG=Lake LEAN_PATH=./build bin LINK_OPTS=-rdynamic "$@"