fix(util/stackinfo): lazy thread initialization

We also add a multithread example for the C API.
This example reproduces a problem reported by Joe Hendrix.

src/tests/shared/CMakeLists.txt

@@ -34,4 +34,12 @@ add_test(ENV c_env_test
          WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
          COMMAND "${CMAKE_CURRENT_BINARY_DIR}/c_env_test")
 SET_TESTS_PROPERTIES(ENV
-  PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_SOURCE_DIR}/../library")
+  PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_SOURCE_DIR}/../library")
+
+add_executable(thread_test thread.cpp)
+target_link_libraries(thread_test ${EXTRA_LIBS} leanshared)
+add_test(thread_test thread_test
+         WORKING_DIRECTORY "${LEAN_BINARY_DIR}"
+         COMMAND "${CMAKE_CURRENT_BINARY_DIR}/thread_test")
+SET_TESTS_PROPERTIES(thread_test
+  PROPERTIES ENVIRONMENT "LEAN_PATH=${LEAN_SOURCE_DIR}/../library")

src/tests/shared/thread.cpp

@@ -0,0 +1,69 @@
+/*
+Copyright (c) 2015 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include <thread>
+#include <iostream>
+#include "api/lean.h"
+
+void check_core(int v, unsigned l) {
+    if (!v) {
+        printf("Test failed at line %d\n", l);
+        exit(1);
+    }
+}
+
+#define check(v) check_core(v, __LINE__)
+
+lean_name mk_name(char const * n) {
+    lean_exception ex;
+    lean_name a, r;
+    check(lean_name_mk_anonymous(&a, &ex));
+    check(lean_name_mk_str(a, n, &r, &ex));
+    lean_name_del(a);
+    return r;
+}
+
+lean_list_name mk_unary_name_list(lean_name u) {
+    lean_exception ex;
+    lean_list_name n, r;
+    check(lean_list_name_mk_nil(&n, &ex));
+    check(lean_list_name_mk_cons(u, n, &r, &ex));
+    lean_list_name_del(n);
+    return r;
+}
+
+lean_env mk_env() {
+    lean_exception ex;
+    lean_env r;
+    check(lean_env_mk_std(LEAN_TRUST_HIGH, &r, &ex));
+    return r;
+}
+
+void test_import() {
+    lean_exception ex;
+    lean_env  env     = mk_env();
+    lean_name std     = mk_name("standard");
+    lean_list_name ms = mk_unary_name_list(std);
+    lean_options o;
+    lean_ios ios;
+    lean_env new_env;
+    check(lean_options_mk_empty(&o, &ex));
+    check(lean_ios_mk_std(o, &ios, &ex));
+    check(lean_env_import(env, ios, ms, &new_env, &ex));
+    std::cout << "standard library has been imported\n";
+    lean_env_del(env);
+    lean_env_del(new_env);
+    lean_name_del(std);
+    lean_list_name_del(ms);
+    lean_options_del(o);
+    lean_ios_del(ios);
+}
+
+int main() {
+    std::thread t1(test_import);
+    t1.join();
+    return 0;
+}

src/util/stackinfo.cpp

@@ -97,7 +97,7 @@ size_t get_stack_size(int main) {
 }
 #endif
 
-static bool g_stack_info_init = false;
+LEAN_THREAD_VALUE(bool, g_stack_info_init, false);
 LEAN_THREAD_VALUE(size_t, g_stack_size, 0);
 LEAN_THREAD_VALUE(size_t, g_stack_base, 0);
 
@@ -123,7 +123,9 @@ size_t get_available_stack_size() {
 }
 
 void check_stack(char const * component_name) {
-    if (g_stack_info_init && get_used_stack_size() + LEAN_MIN_STACK_SPACE > g_stack_size)
+    if (!g_stack_info_init)
+        save_stack_info(false);
+    if (get_used_stack_size() + LEAN_MIN_STACK_SPACE > g_stack_size)
         throw stack_space_exception(component_name);
 }
 }