From bc09a53f71431615f3cbb54bde71dc025cc2b147 Mon Sep 17 00:00:00 2001
From: Gabriel Ebner <gebner@gebner.org>
Date: Fri, 16 Dec 2016 13:41:00 -0500
Subject: [PATCH] feat(library/task_queue): add flag to prevent priority
 inversion

---
 src/kernel/environment.cpp    |  1 +
 src/library/mt_task_queue.cpp | 10 ++++++----
 src/util/task_queue.h         |  2 ++
 3 files changed, 9 insertions(+), 4 deletions(-)

diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index d49c2b3569..abcf8b7e4d 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -218,6 +218,7 @@ public:
     environment_check_task(environment const & env) : m_env(env) {}
 
     bool is_tiny() const override { return true; }
+    bool do_priority_inversion() const override { return false; }
 
     void description(std::ostream & out) const override {
         out << "checking environment for incorrect proofs (" << get_module_id() << ")";
diff --git a/src/library/mt_task_queue.cpp b/src/library/mt_task_queue.cpp
index df3914e43e..245d9a103d 100644
--- a/src/library/mt_task_queue.cpp
+++ b/src/library/mt_task_queue.cpp
@@ -268,10 +268,12 @@ bool mt_task_queue::check_deps(generic_task_result const & t) {
     try {
         deps = unwrap(t)->m_task->get_dependencies();
     } catch (...) {}
-    for (auto & dep : deps) {
-        if (dep) {
-            submit_core(dep);
-            bump_prio(dep, get_prio(t));
+    if (unwrap(t)->m_task->do_priority_inversion()) {
+        for (auto & dep : deps) {
+            if (dep) {
+                submit_core(dep);
+                bump_prio(dep, get_prio(t));
+            }
         }
     }
     for (auto & dep : deps) {
diff --git a/src/util/task_queue.h b/src/util/task_queue.h
index d21a7e787f..ad4d4f11ce 100644
--- a/src/util/task_queue.h
+++ b/src/util/task_queue.h
@@ -138,6 +138,8 @@ public:
     virtual std::vector<generic_task_result> get_dependencies() { return {}; }
 
     virtual bool is_tiny() const { return false; }
+    virtual bool do_priority_inversion() const { return true; }
+
     virtual task_kind get_kind() const { return task_kind::elab; }
     virtual pos_info get_pos() const { return get_task_pos(); }