diff --git a/doc/examples/compiler/README.md b/doc/examples/compiler/README.md
index c5645eaca7..e6bd31688b 100644
--- a/doc/examples/compiler/README.md
+++ b/doc/examples/compiler/README.md
@@ -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]`
diff --git a/doc/examples/compiler/test.lean b/doc/examples/compiler/test.lean
index 8ac7b82b7b..f162825b9e 100644
--- a/doc/examples/compiler/test.lean
+++ b/doc/examples/compiler/test.lean
@@ -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