feat(util/thread_script_state): add system_import procedure

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

src/tests/util/CMakeLists.txt

@@ -22,9 +22,6 @@ add_test(options ${CMAKE_CURRENT_BINARY_DIR}/options)
 add_executable(scoped_map scoped_map.cpp)
 target_link_libraries(scoped_map ${EXTRA_LIBS})
 add_test(scoped_map ${CMAKE_CURRENT_BINARY_DIR}/scoped_map)
-add_executable(thread thread.cpp)
-target_link_libraries(thread ${EXTRA_LIBS})
-add_test(thread ${CMAKE_CURRENT_BINARY_DIR}/thread)
 add_executable(memory memory.cpp)
 target_link_libraries(memory ${EXTRA_LIBS})
 add_test(memory ${CMAKE_CURRENT_BINARY_DIR}/memory)
@@ -76,3 +73,12 @@ add_test(trie ${CMAKE_CURRENT_BINARY_DIR}/trie)
 add_executable(lru_cache lru_cache.cpp)
 target_link_libraries(lru_cache ${EXTRA_LIBS})
 add_test(lru_cache ${CMAKE_CURRENT_BINARY_DIR}/lru_cache)
+# thread.cpp used import_test.lua
+add_custom_command(OUTPUT ${CMAKE_CURRENT_BINARY_DIR}/import_test.lua
+  COMMAND ${CMAKE_COMMAND} -E copy ${CMAKE_CURRENT_SOURCE_DIR}/import_test.lua ${CMAKE_CURRENT_BINARY_DIR}/import_test.lua
+  DEPENDS ${CMAKE_CURRENT_SOURCE_DIR}/import_test.lua)
+add_custom_target("import_test" DEPENDS ${CMAKE_CURRENT_BINARY_DIR}/import_test.lua)
+add_executable(thread thread.cpp)
+target_link_libraries(thread ${EXTRA_LIBS})
+add_test(thread ${CMAKE_CURRENT_BINARY_DIR}/thread)
+add_dependencies(thread import_test)

src/tests/util/import_test.lua

@@ -0,0 +1,4 @@
+print("importing test...")
+function fact(x)
+   if x == 0 then return 1 else return x * fact(x-1) end
+end

src/tests/util/thread.cpp

@@ -175,6 +175,7 @@ static void tst6() {
 
 static void tst7() {
     std::cout << "start\n";
+    system_import("import_test.lua");
     system_dostring("print('hello'); x = 10;");
     interruptible_thread t1([]() {
             script_state S = get_thread_script_state();
@@ -204,7 +205,8 @@ static void tst8() {
                        "for i = 1, 10000 do\n"
                        "  x = x + 1\n"
                        "end\n"
-                       "print(x)\n");
+                       "print(x)\n"
+                       "print(fact(10))\n");
         });
     t1.join();
 }

src/util/thread_script_state.cpp

@@ -5,13 +5,15 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
+#include <utility>
 #include <string>
 #include "util/thread.h"
+#include "util/pair.h"
 #include "util/script_state.h"
 
 namespace lean {
 static mutex g_code_mutex;
-static std::vector<std::string>  g_code;
+static std::vector<std::pair<bool, std::string>> g_code;
 static mutex g_state_mutex;
 static std::vector<script_state> g_states;
 static std::vector<script_state> g_available_states;
@@ -28,7 +30,23 @@ void system_dostring(char const * code) {
     {
         // Save code for future states
         lock_guard<mutex> lk(g_code_mutex);
-        g_code.push_back(code);
+        g_code.push_back(mk_pair(true, code));
+    }
+}
+
+/** \brief Import \c fname in all states in the pool */
+void system_import(char const * fname) {
+    {
+        // Import file in all existing states
+        lock_guard<mutex> lk(g_state_mutex);
+        for (auto & s : g_states) {
+            s.import(fname);
+        }
+    }
+    {
+        // Save module for future states
+        lock_guard<mutex> lk(g_code_mutex);
+        g_code.push_back(mk_pair(false, fname));
     }
 }
 
@@ -47,8 +65,12 @@ static script_state get_state() {
         // Execute existing code in new state
         lock_guard<mutex> lk(g_code_mutex);
         script_state r;
-        for (auto & c : g_code)
-            r.dostring(c.c_str());
+        for (auto const & p : g_code) {
+            if (p.first)
+                r.dostring(p.second.c_str());
+            else
+                r.import(p.second.c_str());
+        }
         g_states.push_back(r);
         {
             // save new state in vector of all states

src/util/thread_script_state.h

@@ -10,12 +10,19 @@ namespace lean {
 /**
     \brief Execute the given piece of code in all global/system script_state objects.
 
-    \remark The code fragments are saved. If a new thread needs to create a new
+    \remark The code fragments are saved. If a thread needs to create a new
     script_state object, all code blocks are executed.
 
     \remark System code should be installed when Lean is started.
 */
 void system_dostring(char const * code);
+/**
+   \brief Import the given module in all global/system script_state objects.
+
+   \remark The module name is saved. If a thread needs to create a new
+   script_state object, all modules are imported.
+*/
+void system_import(char const * fname);
 /**
    \brief Retrieve a script_state object for the current thread.
    The thread has exclusive access until the thread is destroyed,