From 8c30067f8c56b34f000e6e18582388f6cc704062 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 23 Aug 2015 19:08:02 -0700
Subject: [PATCH] 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 | 10 ++++-
 src/tests/shared/thread.cpp     | 69 +++++++++++++++++++++++++++++++++
 src/util/stackinfo.cpp          |  6 ++-
 3 files changed, 82 insertions(+), 3 deletions(-)
 create mode 100644 src/tests/shared/thread.cpp

diff --git a/src/tests/shared/CMakeLists.txt b/src/tests/shared/CMakeLists.txt
index 81f41acaf..8176ea035 100644
--- a/src/tests/shared/CMakeLists.txt
+++ b/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")
\ No newline at end of file
+  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")
diff --git a/src/tests/shared/thread.cpp b/src/tests/shared/thread.cpp
new file mode 100644
index 000000000..744d17299
--- /dev/null
+++ b/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;
+}
diff --git a/src/util/stackinfo.cpp b/src/util/stackinfo.cpp
index 2194b0142..7ead804a2 100644
--- a/src/util/stackinfo.cpp
+++ b/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);
 }
 }