From 886fdf263e34f32714e1ba4461bee6bc3c72d2cd Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 6 Feb 2019 14:50:41 -0800
Subject: [PATCH] chore(doc/examples/compiler): we don't need `main.cpp`
 anymore

cc @kha @ChristianoBraga
---
 doc/examples/compiler/README.md |  9 +++------
 doc/examples/compiler/main.cpp  | 29 -----------------------------
 doc/examples/compiler/test.lean |  9 ++++-----
 3 files changed, 7 insertions(+), 40 deletions(-)
 delete mode 100644 doc/examples/compiler/main.cpp

diff --git a/doc/examples/compiler/README.md b/doc/examples/compiler/README.md
index 6b41ac38a0..c5645eaca7 100644
--- a/doc/examples/compiler/README.md
+++ b/doc/examples/compiler/README.md
@@ -1,7 +1,4 @@
 In this example, we use the Lean C++ code generator to construct a simple program.
-Our project contains two files:
-- `test.lean`: a simple Lean program
-- `main.cpp`: a C++ frontend for invoking the function `foo` defined at `test.lean`.
 
 1- Generate `test.cpp`. Remark: we must have the file `leanpkg.path` in the current directory.
 ```
@@ -10,12 +7,12 @@ Our project contains two files:
 
 2- Generate `test` program using `g++` or `clang++`
 ```
-g++ -o test --std=c++11 -I ../../../src test.cpp main.cpp ../../../bin/libleanstatic.a -lgmp -pthread
+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 100
+./test hello world
 ```
-It should produce `Result: 5050`
+It should produce `Result: [hello, world]`
diff --git a/doc/examples/compiler/main.cpp b/doc/examples/compiler/main.cpp
deleted file mode 100644
index a4d9a76764..0000000000
--- a/doc/examples/compiler/main.cpp
+++ /dev/null
@@ -1,29 +0,0 @@
-#include <iostream>
-#include "runtime/init_module.h"
-#include "runtime/object.h"
-typedef lean::object obj;
-/* Initialization function for the module `test.lean` */
-void initialize_test();
-/* C++ header for the function `foo` at `test.lean` */
-obj* l_foo(obj*);
-
-int main(int argc, char ** argv) {
-    if (argc != 2) {
-        std::cerr << "incorrect number of arguments\n";
-        return 1;
-    }
-    /* Initialize Lean runtime */
-    lean::initialize_runtime_module();
-    /* Initialize module `test.lean` */
-    initialize_test();
-    /* Convert the first argument into a Lean `nat` object */
-    unsigned n = std::atoi(argv[1]);
-    obj * v = lean::mk_nat_obj(n);
-    /* Invoke `foo` defined at `test.lean` */
-    obj * r = l_foo(v);
-    /* Result is a Lean string */
-    std::cout << "Result: " << lean::string_cstr(r) << "\n";
-    /* We use `lean::dec` to consume/dispose the result value. */
-    lean::dec(r);
-    return 0;
-}
diff --git a/doc/examples/compiler/test.lean b/doc/examples/compiler/test.lean
index 27b10fea60..8736eca466 100644
--- a/doc/examples/compiler/test.lean
+++ b/doc/examples/compiler/test.lean
@@ -1,5 +1,4 @@
-def Sum (xs : list nat) : nat :=
-xs.foldl (+) 0
-
-def foo (n : nat) : string :=
-to_string $ Sum (list.iota n)
+@[extname main]
+def my_test (n : list string) : io uint32 :=
+do io.println' (to_string n),
+   pure 0