From fa35fd69898ee5e78ae50e3efee5dd9228b0dab7 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 4 Dec 2013 10:27:18 -0800 Subject: [PATCH] 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 --- src/shell/CMakeLists.txt | 2 +- src/tests/kernel/threads.cpp | 2 +- src/tests/library/tactic/tactic.cpp | 4 +++- src/tests/util/lazy_list.cpp | 2 +- src/tests/util/thread.cpp | 2 +- src/util/interrupt.h | 1 + src/util/lazy_list_fn.h | 7 +++++++ src/util/script_state.cpp | 6 ++++++ 8 files changed, 21 insertions(+), 5 deletions(-) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 14aa28833..7f82c94a8 100644 --- a/src/shell/CMakeLists.txt +++ b/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) diff --git a/src/tests/kernel/threads.cpp b/src/tests/kernel/threads.cpp index d81188079..855f8ea05 100644 --- a/src/tests/kernel/threads.cpp +++ b/src/tests/kernel/threads.cpp @@ -50,7 +50,7 @@ static void tst1() { a = f(a, a); std::vector 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); })); } diff --git a/src/tests/library/tactic/tactic.cpp b/src/tests/library/tactic/tactic.cpp index 0cf56df46..fa9f2bfb5 100644 --- a/src/tests/library/tactic/tactic.cpp +++ b/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()), diff --git a/src/tests/util/lazy_list.cpp b/src/tests/util/lazy_list.cpp index 78d845417..a2b741bae 100644 --- a/src/tests/util/lazy_list.cpp +++ b/src/tests/util/lazy_list.cpp @@ -94,7 +94,7 @@ static void tst1() { display(orelse(lazy_list(), 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 diff --git a/src/tests/util/thread.cpp b/src/tests/util/thread.cpp index 14bbe1b38..c37ec02cd 100644 --- a/src/tests/util/thread.cpp +++ b/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 t2_started(false); diff --git a/src/util/interrupt.h b/src/util/interrupt.h index eb32d88b4..cbf481775 100644 --- a/src/util/interrupt.h +++ b/src/util/interrupt.h @@ -9,6 +9,7 @@ Author: Leonardo de Moura #include #include #include "util/stackinfo.h" +#include "util/exception.h" namespace lean { /** diff --git a/src/util/lazy_list_fn.h b/src/util/lazy_list_fn.h index de5bdff3b..bb610be8b 100644 --- a/src/util/lazy_list_fn.h +++ b/src/util/lazy_list_fn.h @@ -261,6 +261,12 @@ lazy_list timeout(lazy_list 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 +lazy_list par(lazy_list const & l1, lazy_list const & l2, unsigned = g_small_sleep) { + return interleave(l1, l2); +} +#else template lazy_list par(lazy_list const & l1, lazy_list const & l2, unsigned check_ms = g_small_sleep) { return mk_lazy_list([=]() { @@ -313,4 +319,5 @@ lazy_list par(lazy_list const & l1, lazy_list const & l2, unsigned chec } }); } +#endif } diff --git a/src/util/script_state.cpp b/src/util/script_state.cpp index 27bb1b7ba..432a02eba 100644 --- a/src/util/script_state.cpp +++ b/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); } }