chore(*): make sure LEAN_THREAD_UNSAFE build flag is handled correctly

When LEAN_THREAD_UNSAFE=ON, we:

- Do not run tests at tests/lua/threads
- Disable thread object at Lua API
- par tactical becomes an alias for interleave
- Disable some unit tests that use threads

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

src/shell/CMakeLists.txt

@@ -44,7 +44,7 @@ FOREACH(T ${LEANLUADOCS})
 ENDFOREACH(T)
 
 if((${CYGWIN} EQUAL "1") OR (${CMAKE_SYSTEM_NAME} MATCHES "Linux"))
-  if (NOT (${CMAKE_CXX_COMPILER} MATCHES "clang"))
+  if ((NOT (${CMAKE_CXX_COMPILER} MATCHES "clang")) AND (${THREAD_SAFE} MATCHES "ON"))
     file(GLOB LEANLUATHREADTESTS "${LEAN_SOURCE_DIR}/../tests/lua/threads/*.lua")
     FOREACH(T ${LEANLUATHREADTESTS})
       GET_FILENAME_COMPONENT(T_NAME ${T} NAME)

src/tests/kernel/threads.cpp

@@ -50,7 +50,7 @@ static void tst1() {
     a = f(a, a);
     std::vector<std::thread> ts;
 
-    #ifndef __APPLE__
+    #if !defined(__APPLE__) && !defined(LEAN_THREAD_UNSAFE)
     for (unsigned i = 0; i < 8; i++) {
         ts.push_back(std::thread([&](){ save_stack_info(); mk(a); }));
     }

src/tests/library/tactic/tactic.cpp

@@ -65,7 +65,7 @@ static void tst1() {
     check_failure(now_tactic(), env, io, ctx, q);
     std::cout << "proof 2: " << orelse(fail_tactic(), t).solve(env, io, ctx, q).get_proof() << "\n";
 
-#ifndef __APPLE__
+#if !defined(__APPLE__)
     check_failure(try_for(loop_tactic(), 100), env, io, ctx, q);
     std::cout << "proof 1: " << try_for(t, 10000).solve(env, io, s).get_proof() << "\n";
     check_failure(try_for(orelse(try_for(loop_tactic(), 10000),
@@ -83,8 +83,10 @@ static void tst1() {
                          set_tactic(&flag1)),
                   env, io, ctx, q);
     lean_assert(flag1);
+#if !defined(LEAN_THREAD_UNSAFE)
     std::cout << "Before parallel 3 parallel tactics...\n";
     std::cout << "proof 2: " << par(loop_tactic(), par(loop_tactic(), t)).solve(env, io, ctx, q).get_proof() << "\n";
+#endif
 #endif
     std::cout << "Before hello1 and 2...\n";
     std::cout << "proof 2: " << orelse(then(repeat_at_most(append(trace_tactic("hello1"), trace_tactic("hello2")), 5), fail_tactic()),

src/tests/util/lazy_list.cpp

@@ -94,7 +94,7 @@ static void tst1() {
     display(orelse(lazy_list<int>(), take(10, seq(100))));
     display(orelse(take(0, seq(1)), take(10, seq(100))));
     display(orelse(filter(take(100, seq(1)), [](int i) { return i < 0; }), take(10, seq(1000))));
-#ifndef __APPLE__
+#if !defined(__APPLE__) && !defined(LEAN_THREAD_UNSAFE)
     display(timeout(append(append(take(10, seq(1)), loop()), seq(100)), 5));
     display(take(10, par(seq(1), loop())));
 #endif

src/tests/util/thread.cpp

@@ -54,7 +54,7 @@ static void tst2() {
         threads[i].join();
 }
 
-#ifndef __APPLE__
+#if !defined(__APPLE__) && !defined(LEAN_THREAD_UNSAFE)
 static void tst3() {
     shared_mutex      mutex;
     std::atomic<bool> t2_started(false);

src/util/interrupt.h

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include <thread>
 #include <utility>
 #include "util/stackinfo.h"
+#include "util/exception.h"
 
 namespace lean {
 /**

src/util/lazy_list_fn.h

@@ -261,6 +261,12 @@ lazy_list<T> timeout(lazy_list<T> const & l, unsigned ms, unsigned check_ms = g_
    Moreover, when pulling results from the lists, if one finishes before the other,
    then the other one is interrupted.
 */
+#ifdef LEAN_THREAD_UNSAFE
+template<typename T>
+lazy_list<T> par(lazy_list<T> const & l1, lazy_list<T> const & l2, unsigned = g_small_sleep) {
+    return interleave(l1, l2);
+}
+#else
 template<typename T>
 lazy_list<T> par(lazy_list<T> const & l1, lazy_list<T> const & l2, unsigned check_ms = g_small_sleep) {
     return mk_lazy_list<T>([=]() {
@@ -313,4 +319,5 @@ lazy_list<T> par(lazy_list<T> const & l1, lazy_list<T> const & l2, unsigned chec
             }
         });
 }
+#endif
 }

src/util/script_state.cpp

@@ -308,6 +308,7 @@ static void open_state(lua_State * L) {
 #define SMALL_DELAY 10 // in ms
 std::chrono::milliseconds g_small_delay(SMALL_DELAY);
 
+#if !defined(LEAN_THREAD_UNSAFE)
 /**
    \brief Channel for communicating with thread objects in the Lua API
 */
@@ -559,6 +560,7 @@ static void open_thread(lua_State * L) {
     SET_GLOBAL_FUN(mk_thread,   "thread");
     SET_GLOBAL_FUN(thread_pred, "is_thread");
 }
+#endif
 
 static int check_interrupted(lua_State *) { // NOLINT
     check_interrupted();
@@ -586,13 +588,17 @@ static void open_interrupt(lua_State * L) {
     SET_GLOBAL_FUN(check_interrupted, "check_interrupted");
     SET_GLOBAL_FUN(sleep,             "sleep");
     SET_GLOBAL_FUN(yield,             "yield");
+#if !defined(LEAN_THREAD_UNSAFE)
     SET_GLOBAL_FUN(channel_read,      "read");
     SET_GLOBAL_FUN(channel_write,     "write");
+#endif
 }
 
 void open_extra(lua_State * L) {
     open_state(L);
+#if !defined(LEAN_THREAD_UNSAFE)
     open_thread(L);
+#endif
     open_interrupt(L);
 }
 }