doc: port test program instructions to leanmake

This commit is contained in:
Sebastian Ullrich 2020-05-08 17:36:10 +02:00
parent afd7e5fa6e
commit d36c7dc33b
2 changed files with 7 additions and 13 deletions

View file

@ -1,18 +1,12 @@
In this example, we use the Lean C++ code generator to construct a simple program.
In this example, we use the Lean C code generator to construct a simple program.
1- Generate `test.cpp`. Remark: we must have the file `leanpkg.path` in the current directory.
1- Generate `build/bin/test` program using `leanmake` (assuming `bin` from e.g. the stage1 build directory is in your `PATH`)
```
../../../bin/lean --cpp=test.cpp test.lean
leanmake bin PKG=test
```
2- Generate `test` program using `g++` or `clang++`
2- Execute test program
```
g++ -o test --std=c++11 -I ../../../src test.cpp ../../../bin/libleanstatic.a -lgmp -pthread
```
Remark: if you built `libleanstatic.a` using jemalloc, you also need to include option `-ljemalloc` in the previous step.
3- Execute test program
```
./test hello world
./build/bin/test hello world
```
It should produce `Result: [hello, world]`

View file

@ -1,3 +1,3 @@
def main (n : list string) : io uint32 :=
do io.println' (to_string n),
def main (n : List String) : IO UInt32 :=
do IO.println (toString n);
pure 0