chore(doc/examples/compiler): we don't need main.cpp anymore

cc @kha @ChristianoBraga

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]`

doc/examples/compiler/main.cpp

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

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