Remove interrupt.cpp. We changed the way we will handle interruptions in Lean.

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

src/tests/util/CMakeLists.txt

@@ -1,6 +1,3 @@
-add_executable(interrupt interrupt.cpp)
-target_link_libraries(interrupt ${EXTRA_LIBS})
-add_test(interrupt ${CMAKE_CURRENT_BINARY_DIR}/interrupt)
 add_executable(name name.cpp)
 target_link_libraries(name ${EXTRA_LIBS})
 add_test(name ${CMAKE_CURRENT_BINARY_DIR}/name)

src/tests/util/interrupt.cpp

@@ -1,73 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include <iostream>
-#include <chrono>
-#include <mutex>
-#include "interrupt.h"
-#include "test.h"
-
-std::mutex g_stdout_mutex;
-
-static void loop(unsigned i) {
-    try {
-        while (true) {
-            lean::check_interrupt();
-        }
-    }
-    catch (lean::interrupt) {
-        std::lock_guard<std::mutex> lock(g_stdout_mutex);
-        std::cout << "interrupted " << i << ".\n";
-    }
-}
-
-static void tst1() {
-    lean::interruptible_thread t1([](){ loop(1); });
-    lean::interruptible_thread t2([](){ loop(2); });
-
-    std::chrono::milliseconds dura(200);
-    std::this_thread::sleep_for(dura);
-    t2.request_interrupt();
-
-    std::this_thread::sleep_for(dura);
-    t1.request_interrupt();
-
-    t1.join();
-    t2.join();
-}
-
-class A {
-public:
-    unsigned m_x;
-    A():m_x(0) { std::cout << "created...\n"; }
-    ~A() { std::cout << "deleted: " << m_x << "\n"; }
-};
-
-static thread_local A g_a;
-
-static void mka(unsigned x) {
-    std::cout << "starting mka " << x << "\n";
-    g_a.m_x = x;
-}
-
-static void tst2() {
-    {
-        std::thread t1([](){ mka(1); });
-        t1.join();
-    }
-    std::thread t2([](){ mka(2);
-            std::chrono::milliseconds dura(200);
-            std::this_thread::sleep_for(dura);
-        });
-    std::thread t3([](){ mka(3); });
-    t2.join(); t3.join();
-}
-
-int main() {
-    tst1();
-    tst2();
-    return lean::has_violations() ? 1 : 0;
-}

src/util/CMakeLists.txt

@@ -1,2 +1,2 @@
 add_library(util trace.cpp debug.cpp name.cpp exception.cpp
-  interrupt.cpp hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp)
+  hash.cpp escaped.cpp bit_tricks.cpp safe_arith.cpp)

src/util/interrupt.cpp

@@ -1,57 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "interrupt.h"
-
-namespace lean {
-
-thread_local std::atomic_bool g_interrupt;
-
-void request_interrupt() {
-    g_interrupt.store(true);
-}
-
-void reset_interrupt() {
-    g_interrupt.store(false);
-}
-
-bool interrupted() {
-    return g_interrupt.load();
-}
-
-void check_interrupt() {
-    if (interrupted())
-        throw interrupt();
-}
-
-std::atomic_bool * interruptible_thread::get_flag_addr() {
-    return &g_interrupt;
-}
-
-bool interruptible_thread::interrupted() const {
-    std::atomic_bool * f = m_flag_addr.load();
-    if (f == nullptr)
-        return false;
-    return f->load();
-}
-
-bool interruptible_thread::request_interrupt() {
-    std::atomic_bool * f = m_flag_addr.load();
-    if (f == nullptr)
-        return false;
-    f->store(true);
-    return true;
-}
-
-void interruptible_thread::join() {
-    m_thread.join();
-}
-
-bool interruptible_thread::joinable() {
-    return m_thread.joinable();
-}
-
-}

src/util/interrupt.h

@@ -1,77 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#pragma once
-#include <atomic>
-#include <thread>
-#include <utility>
-// APIs for interrupting Lean.
-
-namespace lean {
-
-/**
-   \brief Mark flag for interrupting current thread.
-*/
-void request_interrupt();
-/**
-   \brief Reset (interrupt) flag for current thread.
-*/
-void reset_interrupt();
-
-/**
-   \brief Return true if the
-*/
-bool interrupted();
-
-/**
-   \brief Exception used to sign lean interruptions.
-*/
-class interrupt : public std::exception {
-public:
-    virtual char const * what() const noexcept { return "interrupted"; }
-};
-
-/**
-   \brief Throw an interrupt exception if the (interrupt) flag is set.
-*/
-void check_interrupt();
-
-/**
-   \brief Thread that provides a method for setting its interrupt flag.
-*/
-class interruptible_thread {
-private:
-    std::atomic<std::atomic_bool*> m_flag_addr;
-    std::thread                    m_thread;
-    static std::atomic_bool *      get_flag_addr();
-public:
-    template<typename Function, typename... Args>
-    interruptible_thread(Function && fun, Args &&... args):
-        m_flag_addr(nullptr),
-        m_thread(
-            [&](Function&& fun, Args&&... args) {
-                m_flag_addr.store(get_flag_addr());
-                fun(std::forward<Args>(args)...);
-            },
-            std::forward<Function>(fun),
-            std::forward<Args>(args)...)
-        {}
-
-    /**
-       \brief Return true iff an interrupt request has been made to the current thread.
-     */
-    bool interrupted() const;
-    /**
-       \brief Send a interrupt request to the current thread. Return
-       true iff the request has been successfully performed.
-    */
-    bool request_interrupt();
-
-    void join();
-    bool joinable();
-};
-
-}