diff --git a/src/initialize/init.cpp b/src/initialize/init.cpp
index 753c66065c..71b78495f2 100644
--- a/src/initialize/init.cpp
+++ b/src/initialize/init.cpp
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/stackinfo.h>
-#include <lean/thread.h>
-#include <lean/init_module.h>
+#include "runtime/stackinfo.h"
+#include "runtime/thread.h"
+#include "runtime/init_module.h"
 #include "util/init_module.h"
 #include "util/io.h"
 #include "kernel/init_module.h"
diff --git a/src/kernel/cache_stack.h b/src/kernel/cache_stack.h
index ee66066b8b..1c16f29103 100644
--- a/src/kernel/cache_stack.h
+++ b/src/kernel/cache_stack.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <vector>
 #include <memory>
-#include <lean/debug.h>
+#include "runtime/debug.h"
 
 /** \brief Macro for creating a stack of objects of type Cache in thread local storage.
     The argument \c Arg is provided to every new instance of Cache.
diff --git a/src/kernel/environment.cpp b/src/kernel/environment.cpp
index e2c6513d90..df640f9d24 100644
--- a/src/kernel/environment.cpp
+++ b/src/kernel/environment.cpp
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #include <utility>
 #include <vector>
 #include <limits>
-#include <lean/sstream.h>
-#include <lean/thread.h>
+#include "runtime/sstream.h"
+#include "runtime/thread.h"
 #include "util/map_foreach.h"
 #include "util/io.h"
 #include "kernel/environment.h"
diff --git a/src/kernel/environment.h b/src/kernel/environment.h
index 64456b9905..d9cb69f472 100644
--- a/src/kernel/environment.h
+++ b/src/kernel/environment.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include <memory>
 #include <vector>
-#include <lean/optional.h>
+#include "runtime/optional.h"
 #include "util/rc.h"
 #include "util/list.h"
 #include "util/rb_map.h"
diff --git a/src/kernel/equiv_manager.cpp b/src/kernel/equiv_manager.cpp
index 9f2f148e93..d5dfee859c 100644
--- a/src/kernel/equiv_manager.cpp
+++ b/src/kernel/equiv_manager.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/interrupt.h>
-#include <lean/flet.h>
+#include "runtime/interrupt.h"
+#include "runtime/flet.h"
 #include "kernel/equiv_manager.h"
 
 namespace lean {
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index ff6a92ff49..cf33aebc4c 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -10,8 +10,8 @@ Author: Leonardo de Moura
 #include <string>
 #include <algorithm>
 #include <limits>
-#include <lean/hash.h>
-#include <lean/buffer.h>
+#include "runtime/hash.h"
+#include "runtime/buffer.h"
 #include "util/list_fn.h"
 #include "kernel/expr.h"
 #include "kernel/expr_eq_fn.h"
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index d474d4354f..9e32e65685 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -11,10 +11,10 @@ Author: Leonardo de Moura
 #include <utility>
 #include <tuple>
 #include <string>
-#include <lean/optional.h>
-#include <lean/thread.h>
-#include <lean/hash.h>
-#include <lean/buffer.h>
+#include "runtime/optional.h"
+#include "runtime/thread.h"
+#include "runtime/hash.h"
+#include "runtime/buffer.h"
 #include "util/name.h"
 #include "util/nat.h"
 #include "util/kvmap.h"
diff --git a/src/kernel/expr_eq_fn.cpp b/src/kernel/expr_eq_fn.cpp
index 3192db5897..4c0f9e93d6 100644
--- a/src/kernel/expr_eq_fn.cpp
+++ b/src/kernel/expr_eq_fn.cpp
@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <memory>
-#include <lean/interrupt.h>
-#include <lean/thread.h>
+#include "runtime/interrupt.h"
+#include "runtime/thread.h"
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
 
diff --git a/src/kernel/expr_sets.h b/src/kernel/expr_sets.h
index 08fb5a5606..c9459f35a9 100644
--- a/src/kernel/expr_sets.h
+++ b/src/kernel/expr_sets.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <unordered_set>
 #include <utility>
 #include <functional>
-#include <lean/hash.h>
+#include "runtime/hash.h"
 #include "kernel/expr.h"
 
 namespace lean {
diff --git a/src/kernel/for_each_fn.cpp b/src/kernel/for_each_fn.cpp
index 1f7507b7f1..e8f44df209 100644
--- a/src/kernel/for_each_fn.cpp
+++ b/src/kernel/for_each_fn.cpp
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 */
 #include <vector>
 #include <utility>
-#include <lean/memory.h>
-#include <lean/interrupt.h>
-#include <lean/flet.h>
+#include "runtime/memory.h"
+#include "runtime/interrupt.h"
+#include "runtime/flet.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/cache_stack.h"
 
diff --git a/src/kernel/for_each_fn.h b/src/kernel/for_each_fn.h
index d6a46c96f0..cb5e968604 100644
--- a/src/kernel/for_each_fn.h
+++ b/src/kernel/for_each_fn.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include <utility>
 #include <functional>
-#include <lean/buffer.h>
+#include "runtime/buffer.h"
 #include "kernel/expr.h"
 #include "kernel/expr_sets.h"
 
diff --git a/src/kernel/inductive.cpp b/src/kernel/inductive.cpp
index 3d1a47659b..3522201b91 100644
--- a/src/kernel/inductive.cpp
+++ b/src/kernel/inductive.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/sstream.h>
-#include <lean/utf8.h>
+#include "runtime/sstream.h"
+#include "runtime/utf8.h"
 #include "util/name_generator.h"
 #include "kernel/environment.h"
 #include "kernel/type_checker.h"
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index c817336502..527445ec17 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -8,10 +8,10 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <vector>
 #include <unordered_set>
-#include <lean/debug.h>
-#include <lean/interrupt.h>
-#include <lean/hash.h>
-#include <lean/buffer.h>
+#include "runtime/debug.h"
+#include "runtime/interrupt.h"
+#include "runtime/hash.h"
+#include "runtime/buffer.h"
 #include "util/list.h"
 #include "kernel/level.h"
 #include "kernel/environment.h"
diff --git a/src/kernel/level.h b/src/kernel/level.h
index fb5ea145f4..cedabf02fb 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include <iostream>
 #include <algorithm>
 #include <utility>
-#include <lean/optional.h>
-#include <lean/list_ref.h>
+#include "runtime/optional.h"
+#include "runtime/list_ref.h"
 #include "util/name.h"
 #include "util/options.h"
 #include "util/format.h"
diff --git a/src/kernel/local_ctx.cpp b/src/kernel/local_ctx.cpp
index 8849505dec..3d2d0305cb 100644
--- a/src/kernel/local_ctx.cpp
+++ b/src/kernel/local_ctx.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "kernel/local_ctx.h"
 #include "kernel/abstract.h"
 
diff --git a/src/kernel/replace_fn.h b/src/kernel/replace_fn.h
index f60232d4c4..ed2d8f9d39 100644
--- a/src/kernel/replace_fn.h
+++ b/src/kernel/replace_fn.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <tuple>
-#include <lean/interrupt.h>
+#include "runtime/interrupt.h"
 #include "kernel/expr.h"
 #include "kernel/expr_maps.h"
 
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index d97a80a610..56881dcd46 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 */
 #include <utility>
 #include <vector>
-#include <lean/interrupt.h>
-#include <lean/sstream.h>
-#include <lean/flet.h>
+#include "runtime/interrupt.h"
+#include "runtime/sstream.h"
+#include "runtime/flet.h"
 #include "util/lbool.h"
 #include "kernel/type_checker.h"
 #include "kernel/expr_maps.h"
diff --git a/src/library/annotation.cpp b/src/library/annotation.cpp
index 887bbc33a3..b482d819b3 100644
--- a/src/library/annotation.cpp
+++ b/src/library/annotation.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <unordered_map>
 #include <memory>
 #include <string>
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "util/name_hash_map.h"
 #include "library/annotation.h"
 
diff --git a/src/library/compiler/cse.cpp b/src/library/compiler/cse.cpp
index f07b8c6737..d2fd28946d 100644
--- a/src/library/compiler/cse.cpp
+++ b/src/library/compiler/cse.cpp
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include <vector>
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "util/name_generator.h"
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
diff --git a/src/library/compiler/csimp.cpp b/src/library/compiler/csimp.cpp
index 2a90459ff3..81fed326a9 100644
--- a/src/library/compiler/csimp.cpp
+++ b/src/library/compiler/csimp.cpp
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <unordered_set>
 #include <unordered_map>
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "kernel/type_checker.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
diff --git a/src/library/compiler/eager_lambda_lifting.cpp b/src/library/compiler/eager_lambda_lifting.cpp
index c65e9153ec..65148ca18f 100644
--- a/src/library/compiler/eager_lambda_lifting.cpp
+++ b/src/library/compiler/eager_lambda_lifting.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
diff --git a/src/library/compiler/erase_irrelevant.cpp b/src/library/compiler/erase_irrelevant.cpp
index c57dde090b..63da01a73c 100644
--- a/src/library/compiler/erase_irrelevant.cpp
+++ b/src/library/compiler/erase_irrelevant.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
diff --git a/src/library/compiler/extern_attribute.cpp b/src/library/compiler/extern_attribute.cpp
index 82c8be0317..e8dd0d0b20 100644
--- a/src/library/compiler/extern_attribute.cpp
+++ b/src/library/compiler/extern_attribute.cpp
@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Authors: Leonardo de Moura
 */
 #include <string>
-#include <lean/sstream.h>
-#include <lean/object_ref.h>
-#include <lean/option_ref.h>
+#include "runtime/sstream.h"
+#include "runtime/object_ref.h"
+#include "runtime/option_ref.h"
 #include "util/io.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
diff --git a/src/library/compiler/extract_closed.cpp b/src/library/compiler/extract_closed.cpp
index 1d6ba27cfd..ed3e10facc 100644
--- a/src/library/compiler/extract_closed.cpp
+++ b/src/library/compiler/extract_closed.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "kernel/instantiate.h"
 #include "kernel/expr_maps.h"
 #include "kernel/for_each_fn.h"
diff --git a/src/library/compiler/init_attribute.cpp b/src/library/compiler/init_attribute.cpp
index ac2fdff23f..eac9ad41f1 100644
--- a/src/library/compiler/init_attribute.cpp
+++ b/src/library/compiler/init_attribute.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Authors: Leonardo de Moura
 */
-#include <lean/object_ref.h>
+#include "runtime/object_ref.h"
 #include "kernel/environment.h"
 
 namespace lean {
diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp
index 7aae55a83e..bcb7191ed1 100644
--- a/src/library/compiler/ir.cpp
+++ b/src/library/compiler/ir.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
-#include <lean/array_ref.h>
+#include "runtime/array_ref.h"
 #include "util/nat.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
diff --git a/src/library/compiler/ir_interpreter.cpp b/src/library/compiler/ir_interpreter.cpp
index 91dd9e7e4a..9b6675d39e 100644
--- a/src/library/compiler/ir_interpreter.cpp
+++ b/src/library/compiler/ir_interpreter.cpp
@@ -35,12 +35,12 @@ functions, which have a (relatively) homogeneous ABI that we can use without run
 #else
 #include <dlfcn.h>
 #endif
-#include <lean/flet.h>
-#include <lean/apply.h>
-#include <lean/interrupt.h>
-#include <lean/io.h>
-#include <lean/option_ref.h>
-#include <lean/array_ref.h>
+#include "runtime/flet.h"
+#include "runtime/apply.h"
+#include "runtime/interrupt.h"
+#include "runtime/io.h"
+#include "runtime/option_ref.h"
+#include "runtime/array_ref.h"
 #include "library/time_task.h"
 #include "library/trace.h"
 #include "library/compiler/ir.h"
diff --git a/src/library/compiler/ir_interpreter.h b/src/library/compiler/ir_interpreter.h
index 3fdc49b40d..722d809c0b 100644
--- a/src/library/compiler/ir_interpreter.h
+++ b/src/library/compiler/ir_interpreter.h
@@ -6,7 +6,7 @@ Author: Sebastian Ullrich
 */
 #pragma once
 #include "kernel/environment.h"
-#include <lean/object.h>
+#include "runtime/object.h"
 
 namespace lean {
 namespace ir {
diff --git a/src/library/compiler/lambda_lifting.cpp b/src/library/compiler/lambda_lifting.cpp
index ca36ddde23..2889fcc385 100644
--- a/src/library/compiler/lambda_lifting.cpp
+++ b/src/library/compiler/lambda_lifting.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <unordered_set>
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/for_each_fn.h"
diff --git a/src/library/compiler/lcnf.cpp b/src/library/compiler/lcnf.cpp
index 08410e1883..0459e38cde 100644
--- a/src/library/compiler/lcnf.cpp
+++ b/src/library/compiler/lcnf.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
-#include <lean/flet.h>
-#include <lean/sstream.h>
+#include "runtime/flet.h"
+#include "runtime/sstream.h"
 #include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive.h"
diff --git a/src/library/compiler/ll_infer_type.cpp b/src/library/compiler/ll_infer_type.cpp
index 71e1202732..8bc7c684ae 100644
--- a/src/library/compiler/ll_infer_type.cpp
+++ b/src/library/compiler/ll_infer_type.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/sstream.h>
-#include <lean/flet.h>
+#include "runtime/sstream.h"
+#include "runtime/flet.h"
 #include "kernel/instantiate.h"
 #include "kernel/replace_fn.h"
 #include "library/compiler/util.h"
diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index 46f5bb6d69..8489fe4c0f 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include <vector>
 #include <algorithm>
 #include <unordered_set>
-#include <lean/flet.h>
-#include <lean/sstream.h>
+#include "runtime/flet.h"
+#include "runtime/sstream.h"
 #include "util/name_hash_set.h"
 #include "util/name_hash_map.h"
 #include "kernel/instantiate.h"
diff --git a/src/library/compiler/specialize.cpp b/src/library/compiler/specialize.cpp
index 7021a6fdf3..1cbae1568f 100644
--- a/src/library/compiler/specialize.cpp
+++ b/src/library/compiler/specialize.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <algorithm>
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "kernel/instantiate.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
diff --git a/src/library/compiler/struct_cases_on.cpp b/src/library/compiler/struct_cases_on.cpp
index f82a56fa59..b917202a39 100644
--- a/src/library/compiler/struct_cases_on.cpp
+++ b/src/library/compiler/struct_cases_on.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/flet.h>
+#include "runtime/flet.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
diff --git a/src/library/compiler/util.h b/src/library/compiler/util.h
index 454fec4ef4..eab67d115a 100644
--- a/src/library/compiler/util.h
+++ b/src/library/compiler/util.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/pair_ref.h>
-#include <lean/list_ref.h>
+#include "runtime/pair_ref.h"
+#include "runtime/list_ref.h"
 #include "util/name_hash_set.h"
 #include "kernel/expr.h"
 #include "kernel/type_checker.h"
diff --git a/src/library/constructions/brec_on.cpp b/src/library/constructions/brec_on.cpp
index 83427bc908..dfdebaf7ab 100644
--- a/src/library/constructions/brec_on.cpp
+++ b/src/library/constructions/brec_on.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
diff --git a/src/library/constructions/cases_on.cpp b/src/library/constructions/cases_on.cpp
index 0d1c3ac30a..e383687dbf 100644
--- a/src/library/constructions/cases_on.cpp
+++ b/src/library/constructions/cases_on.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
diff --git a/src/library/constructions/no_confusion.cpp b/src/library/constructions/no_confusion.cpp
index 125aec4462..cee34aa046 100644
--- a/src/library/constructions/no_confusion.cpp
+++ b/src/library/constructions/no_confusion.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
diff --git a/src/library/constructions/projection.cpp b/src/library/constructions/projection.cpp
index c04e5ef422..352ee3a6ed 100644
--- a/src/library/constructions/projection.cpp
+++ b/src/library/constructions/projection.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/abstract.h"
 #include "kernel/type_checker.h"
diff --git a/src/library/constructions/rec_on.cpp b/src/library/constructions/rec_on.cpp
index 70a896ab49..b9210db613 100644
--- a/src/library/constructions/rec_on.cpp
+++ b/src/library/constructions/rec_on.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/environment.h"
 #include "kernel/instantiate.h"
diff --git a/src/library/expr_pair.h b/src/library/expr_pair.h
index f476ef258e..b53660febd 100644
--- a/src/library/expr_pair.h
+++ b/src/library/expr_pair.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <utility>
-#include <lean/hash.h>
+#include "runtime/hash.h"
 #include "library/expr_lt.h"
 
 namespace lean {
diff --git a/src/library/max_sharing.cpp b/src/library/max_sharing.cpp
index f73509a039..ae43ae5a87 100644
--- a/src/library/max_sharing.cpp
+++ b/src/library/max_sharing.cpp
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #include <tuple>
 #include <unordered_set>
 #include <functional>
-#include <lean/interrupt.h>
-#include <lean/buffer.h>
+#include "runtime/interrupt.h"
+#include "runtime/buffer.h"
 #include "library/max_sharing.h"
 
 namespace lean {
diff --git a/src/library/module.cpp b/src/library/module.cpp
index 7c6c2b3713..797464a75a 100644
--- a/src/library/module.cpp
+++ b/src/library/module.cpp
@@ -12,13 +12,13 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 #include <fstream>
 #include <algorithm>
 #include <sys/stat.h>
-#include <lean/thread.h>
-#include <lean/interrupt.h>
-#include <lean/sstream.h>
-#include <lean/hash.h>
-#include <lean/io.h>
-#include <lean/compact.h>
-#include <lean/buffer.h>
+#include "runtime/thread.h"
+#include "runtime/interrupt.h"
+#include "runtime/sstream.h"
+#include "runtime/hash.h"
+#include "runtime/io.h"
+#include "runtime/compact.h"
+#include "runtime/buffer.h"
 #include "util/io.h"
 #include "util/name_map.h"
 #include "library/module.h"
diff --git a/src/library/module.h b/src/library/module.h
index 60d8ba6dd9..9ab3b51b2e 100644
--- a/src/library/module.h
+++ b/src/library/module.h
@@ -9,7 +9,7 @@ Authors: Leonardo de Moura, Gabriel Ebner, Sebastian Ullrich
 #include <iostream>
 #include <utility>
 #include <vector>
-#include <lean/optional.h>
+#include "runtime/optional.h"
 #include "kernel/environment.h"
 
 namespace lean {
diff --git a/src/library/num.h b/src/library/num.h
index edb8caa6c5..4528d9efa1 100644
--- a/src/library/num.h
+++ b/src/library/num.h
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/mpz.h>
+#include "runtime/mpz.h"
 #include "kernel/environment.h"
 
 namespace lean {
diff --git a/src/library/projection.cpp b/src/library/projection.cpp
index 5efaaeb8c9..cae5d6201e 100644
--- a/src/library/projection.cpp
+++ b/src/library/projection.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <string>
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/instantiate.h"
 #include "kernel/inductive.h"
diff --git a/src/library/replace_visitor.cpp b/src/library/replace_visitor.cpp
index be3f90b995..55360e8ca8 100644
--- a/src/library/replace_visitor.cpp
+++ b/src/library/replace_visitor.cpp
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <tuple>
-#include <lean/interrupt.h>
+#include "runtime/interrupt.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
 #include "library/replace_visitor.h"
diff --git a/src/library/util.cpp b/src/library/util.cpp
index 3bd9c12047..bc7cd5a016 100644
--- a/src/library/util.cpp
+++ b/src/library/util.cpp
@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 */
 #include <algorithm>
 #include <string>
-#include <lean/option_ref.h>
 #include <lean/version.h>
+#include "runtime/option_ref.h"
 #include "kernel/find_fn.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
diff --git a/src/runtime/alloc.cpp b/src/runtime/alloc.cpp
index 5aa606d8fb..74ed3d7651 100644
--- a/src/runtime/alloc.cpp
+++ b/src/runtime/alloc.cpp
@@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
-#include <lean/thread.h>
-#include <lean/debug.h>
-#include <lean/alloc.h>
 #include <lean/lean.h>
+#include "runtime/thread.h"
+#include "runtime/debug.h"
+#include "runtime/alloc.h"
 
 #if defined(__GNUC__) || defined(__clang__)
 #define LEAN_NOINLINE __attribute__((noinline))
diff --git a/src/include/lean/alloc.h b/src/runtime/alloc.h
similarity index 100%
rename from src/include/lean/alloc.h
rename to src/runtime/alloc.h
diff --git a/src/runtime/allocprof.cpp b/src/runtime/allocprof.cpp
index 3eed2efaa3..7eeedf3df2 100644
--- a/src/runtime/allocprof.cpp
+++ b/src/runtime/allocprof.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/allocprof.h>
+#include "runtime/allocprof.h"
 namespace lean {
 allocprof::allocprof(std::ostream & out, char const * msg):
     m_out(out), m_msg(msg) {
diff --git a/src/include/lean/allocprof.h b/src/runtime/allocprof.h
similarity index 95%
rename from src/include/lean/allocprof.h
rename to src/runtime/allocprof.h
index ca07aa4390..5de1ca798a 100644
--- a/src/include/lean/allocprof.h
+++ b/src/runtime/allocprof.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
-#include <lean/object.h>
+#include "runtime/object.h"
 namespace lean {
 /* Low tech runtime allocation profiler.
    We need to compile Lean using RUNTIME_STATS=ON to use it. */
diff --git a/src/runtime/apply.cpp b/src/runtime/apply.cpp
index cf026579de..46a5c8d7da 100644
--- a/src/runtime/apply.cpp
+++ b/src/runtime/apply.cpp
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 // DO NOT EDIT, this is an automatically generated file
 // Generated using script: ../../gen/apply.lean
-#include <lean/apply.h>
+#include "runtime/apply.h"
 namespace lean {
 #define obj lean_object
 #define fx(i) lean_closure_arg_cptr(f)[i]
diff --git a/src/include/lean/apply.h b/src/runtime/apply.h
similarity index 89%
rename from src/include/lean/apply.h
rename to src/runtime/apply.h
index b6650ac70f..7a08d58d1c 100644
--- a/src/include/lean/apply.h
+++ b/src/runtime/apply.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/object.h>
+#include "runtime/object.h"
 namespace lean {
 object * curry(void * f, unsigned n, object ** as);
 }
diff --git a/src/include/lean/array_ref.h b/src/runtime/array_ref.h
similarity index 97%
rename from src/include/lean/array_ref.h
rename to src/runtime/array_ref.h
index e499ffdc1d..a0f4db4450 100644
--- a/src/include/lean/array_ref.h
+++ b/src/runtime/array_ref.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/buffer.h>
-#include <lean/object_ref.h>
+#include "runtime/buffer.h"
+#include "runtime/object_ref.h"
 
 namespace lean {
 template<typename C> object * to_array(C const & elems) {
diff --git a/src/include/lean/buffer.h b/src/runtime/buffer.h
similarity index 98%
rename from src/include/lean/buffer.h
rename to src/runtime/buffer.h
index a7ed0caa5f..8d41ec447b 100644
--- a/src/include/lean/buffer.h
+++ b/src/runtime/buffer.h
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include <algorithm>
 #include <cstring>
-#include <lean/debug.h>
-#include <lean/optional.h>
+#include "runtime/debug.h"
+#include "runtime/optional.h"
 
 namespace lean {
 /**
diff --git a/src/runtime/compact.cpp b/src/runtime/compact.cpp
index dabd9eaf75..b68cd3bec4 100644
--- a/src/runtime/compact.cpp
+++ b/src/runtime/compact.cpp
@@ -8,9 +8,9 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <string>
 #include <vector>
-#include <lean/hash.h>
 #include <lean/lean.h>
-#include <lean/compact.h>
+#include "runtime/hash.h"
+#include "runtime/compact.h"
 
 #ifndef LEAN_WINDOWS
 #include <sys/mman.h>
diff --git a/src/include/lean/compact.h b/src/runtime/compact.h
similarity index 99%
rename from src/include/lean/compact.h
rename to src/runtime/compact.h
index 47e17b0b7b..8664c0614d 100644
--- a/src/include/lean/compact.h
+++ b/src/runtime/compact.h
@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <functional>
 #include <vector>
 #include <unordered_map>
-#include <lean/object.h>
+#include "runtime/object.h"
 
 namespace lean {
 typedef lean_object * object_offset;
diff --git a/src/runtime/debug.cpp b/src/runtime/debug.cpp
index 72d6667e13..7317464a32 100644
--- a/src/runtime/debug.cpp
+++ b/src/runtime/debug.cpp
@@ -17,7 +17,7 @@ Author: Leonardo de Moura
 // Support for pid
 #include<unistd.h>
 #endif
-#include <lean/debug.h>
+#include "runtime/debug.h"
 
 namespace lean {
 static volatile bool           g_has_violations     = false;
diff --git a/src/include/lean/debug.h b/src/runtime/debug.h
similarity index 99%
rename from src/include/lean/debug.h
rename to src/runtime/debug.h
index 8e63f3be70..d3d857a66f 100644
--- a/src/include/lean/debug.h
+++ b/src/runtime/debug.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <typeinfo>
-#include <lean/exception.h>
+#include "runtime/exception.h"
 
 #ifndef __has_builtin
 #define __has_builtin(x) 0
diff --git a/src/runtime/exception.cpp b/src/runtime/exception.cpp
index 03c2ca34dc..7e6d13d1e0 100644
--- a/src/runtime/exception.cpp
+++ b/src/runtime/exception.cpp
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 */
 #include <string>
 #include <sstream>
-#include <lean/exception.h>
-#include <lean/thread.h>
-#include <lean/sstream.h>
+#include "runtime/exception.h"
+#include "runtime/thread.h"
+#include "runtime/sstream.h"
 
 namespace lean {
 throwable::throwable(char const * msg):m_msg(msg) {}
diff --git a/src/include/lean/exception.h b/src/runtime/exception.h
similarity index 100%
rename from src/include/lean/exception.h
rename to src/runtime/exception.h
diff --git a/src/include/lean/flet.h b/src/runtime/flet.h
similarity index 100%
rename from src/include/lean/flet.h
rename to src/runtime/flet.h
diff --git a/src/include/lean/hash.h b/src/runtime/hash.h
similarity index 97%
rename from src/include/lean/hash.h
rename to src/runtime/hash.h
index 88d57d467d..7b0775e7d5 100644
--- a/src/include/lean/hash.h
+++ b/src/runtime/hash.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/debug.h>
-#include <lean/int64.h>
+#include "runtime/debug.h"
+#include "runtime/int64.h"
 
 namespace lean {
 
diff --git a/src/runtime/init_module.cpp b/src/runtime/init_module.cpp
index 84d96aa3b3..ec166b3d2c 100644
--- a/src/runtime/init_module.cpp
+++ b/src/runtime/init_module.cpp
@@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/alloc.h>
-#include <lean/debug.h>
-#include <lean/thread.h>
-#include <lean/object.h>
-#include <lean/io.h>
-#include <lean/stack_overflow.h>
-#include <lean/process.h>
+#include "runtime/alloc.h"
+#include "runtime/debug.h"
+#include "runtime/thread.h"
+#include "runtime/object.h"
+#include "runtime/io.h"
+#include "runtime/stack_overflow.h"
+#include "runtime/process.h"
 
 namespace lean {
 extern "C" void lean_initialize_runtime_module() {
diff --git a/src/include/lean/init_module.h b/src/runtime/init_module.h
similarity index 100%
rename from src/include/lean/init_module.h
rename to src/runtime/init_module.h
diff --git a/src/include/lean/int64.h b/src/runtime/int64.h
similarity index 100%
rename from src/include/lean/int64.h
rename to src/runtime/int64.h
diff --git a/src/runtime/interrupt.cpp b/src/runtime/interrupt.cpp
index b887a83304..17ac6aeb0e 100644
--- a/src/runtime/interrupt.cpp
+++ b/src/runtime/interrupt.cpp
@@ -5,10 +5,10 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <limits>
-#include <lean/thread.h>
-#include <lean/interrupt.h>
-#include <lean/exception.h>
-#include <lean/memory.h>
+#include "runtime/thread.h"
+#include "runtime/interrupt.h"
+#include "runtime/exception.h"
+#include "runtime/memory.h"
 
 namespace lean {
 LEAN_THREAD_VALUE(size_t, g_max_heartbeat, 0);
diff --git a/src/include/lean/interrupt.h b/src/runtime/interrupt.h
similarity index 95%
rename from src/include/lean/interrupt.h
rename to src/runtime/interrupt.h
index 467082dee7..6629513410 100644
--- a/src/include/lean/interrupt.h
+++ b/src/runtime/interrupt.h
@@ -6,10 +6,10 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <utility>
-#include <lean/thread.h>
-#include <lean/stackinfo.h>
-#include <lean/exception.h>
-#include <lean/flet.h>
+#include "runtime/thread.h"
+#include "runtime/stackinfo.h"
+#include "runtime/exception.h"
+#include "runtime/flet.h"
 
 namespace lean {
 /** \brief Increment thread local counter for approximating elapsed time. */
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 3dc9b91755..fb06bdefad 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -36,12 +36,12 @@ Authors: Leonardo de Moura, Sebastian Ullrich
 #include <cctype>
 #include <sys/stat.h>
 #include "util/io.h"
-#include <lean/alloc.h>
-#include <lean/io.h>
-#include <lean/utf8.h>
-#include <lean/object.h>
-#include <lean/thread.h>
-#include <lean/allocprof.h>
+#include "runtime/alloc.h"
+#include "runtime/io.h"
+#include "runtime/utf8.h"
+#include "runtime/object.h"
+#include "runtime/thread.h"
+#include "runtime/allocprof.h"
 
 #ifdef _MSC_VER
 #define S_ISDIR(mode) ((mode & _S_IFDIR) != 0)
diff --git a/src/include/lean/io.h b/src/runtime/io.h
similarity index 100%
rename from src/include/lean/io.h
rename to src/runtime/io.h
diff --git a/src/include/lean/list_ref.h b/src/runtime/list_ref.h
similarity index 99%
rename from src/include/lean/list_ref.h
rename to src/runtime/list_ref.h
index 3fc3703ca5..19aa342a6f 100644
--- a/src/include/lean/list_ref.h
+++ b/src/runtime/list_ref.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/buffer.h>
-#include <lean/object_ref.h>
+#include "runtime/buffer.h"
+#include "runtime/object_ref.h"
 
 namespace lean {
 template<typename T> T const & head(object * o) { return static_cast<T const &>(cnstr_get_ref(o, 0)); }
diff --git a/src/runtime/memory.cpp b/src/runtime/memory.cpp
index 3b787f4121..876e777767 100644
--- a/src/runtime/memory.cpp
+++ b/src/runtime/memory.cpp
@@ -7,9 +7,9 @@ Author: Leonardo de Moura
 #include <new>
 #include <cstdlib>
 #include <iostream>
-#include <lean/exception.h>
-#include <lean/memory.h>
-#include <lean/thread.h>
+#include "runtime/exception.h"
+#include "runtime/memory.h"
+#include "runtime/thread.h"
 
 #ifndef LEAN_CHECK_MEM_THRESHOLD
 #define LEAN_CHECK_MEM_THRESHOLD 200
diff --git a/src/include/lean/memory.h b/src/runtime/memory.h
similarity index 100%
rename from src/include/lean/memory.h
rename to src/runtime/memory.h
diff --git a/src/runtime/mpq.cpp b/src/runtime/mpq.cpp
index 07af2a378c..14183647e1 100644
--- a/src/runtime/mpq.cpp
+++ b/src/runtime/mpq.cpp
@@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/thread.h>
-#include <lean/mpq.h>
-#include <lean/sstream.h>
+#include "runtime/thread.h"
+#include "runtime/mpq.h"
+#include "runtime/sstream.h"
 
 namespace lean {
 MK_THREAD_LOCAL_GET_DEF(mpz, get_tlocal1);
diff --git a/src/include/lean/mpq.h b/src/runtime/mpq.h
similarity index 99%
rename from src/include/lean/mpq.h
rename to src/runtime/mpq.h
index daeaee258c..bb0e4d4064 100644
--- a/src/include/lean/mpq.h
+++ b/src/runtime/mpq.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/mpz.h>
+#include "runtime/mpz.h"
 
 namespace lean {
 /**
diff --git a/src/runtime/mpz.cpp b/src/runtime/mpz.cpp
index 35efa4b7a6..0d27cfab45 100644
--- a/src/runtime/mpz.cpp
+++ b/src/runtime/mpz.cpp
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 */
 #include <memory>
 #include <string>
-#include <lean/sstream.h>
-#include <lean/thread.h>
-#include <lean/mpz.h>
+#include "runtime/sstream.h"
+#include "runtime/thread.h"
+#include "runtime/mpz.h"
 
 namespace lean {
 mpz::mpz(uint64 v):
diff --git a/src/include/lean/mpz.h b/src/runtime/mpz.h
similarity index 99%
rename from src/include/lean/mpz.h
rename to src/runtime/mpz.h
index a6f87c53b9..a6e8354bc6 100644
--- a/src/include/lean/mpz.h
+++ b/src/runtime/mpz.h
@@ -10,9 +10,9 @@ Author: Leonardo de Moura
 #include <string>
 #include <iostream>
 #include <limits>
-#include <lean/int64.h>
-#include <lean/debug.h>
 #include <lean/lean.h>
+#include "runtime/int64.h"
+#include "runtime/debug.h"
 
 namespace lean {
 
diff --git a/src/runtime/object.cpp b/src/runtime/object.cpp
index 0ec22f84cc..d95a3cdacb 100644
--- a/src/runtime/object.cpp
+++ b/src/runtime/object.cpp
@@ -9,16 +9,16 @@ Author: Leonardo de Moura
 #include <vector>
 #include <deque>
 #include <cmath>
-#include <lean/object.h>
-#include <lean/mpq.h>
-#include <lean/thread.h>
-#include <lean/utf8.h>
-#include <lean/alloc.h>
-#include <lean/debug.h>
-#include <lean/hash.h>
-#include <lean/flet.h>
-#include <lean/interrupt.h>
-#include <lean/buffer.h>
+#include "runtime/object.h"
+#include "runtime/mpq.h"
+#include "runtime/thread.h"
+#include "runtime/utf8.h"
+#include "runtime/alloc.h"
+#include "runtime/debug.h"
+#include "runtime/hash.h"
+#include "runtime/flet.h"
+#include "runtime/interrupt.h"
+#include "runtime/buffer.h"
 
 // see `Task.Priority.max`
 #define LEAN_MAX_PRIO 8
diff --git a/src/include/lean/object.h b/src/runtime/object.h
similarity index 99%
rename from src/include/lean/object.h
rename to src/runtime/object.h
index 210fefeb38..38613cf47c 100644
--- a/src/include/lean/object.h
+++ b/src/runtime/object.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <string>
 #include <lean/lean.h>
-#include <lean/mpz.h>
+#include "runtime/mpz.h"
 
 namespace lean {
 typedef uint8_t  uint8;
diff --git a/src/runtime/object_ref.cpp b/src/runtime/object_ref.cpp
index 1bd6ee66ef..a889b22859 100644
--- a/src/runtime/object_ref.cpp
+++ b/src/runtime/object_ref.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/object_ref.h>
+#include "runtime/object_ref.h"
 
 namespace lean {
 object_ref mk_cnstr(unsigned tag, unsigned num_objs, object ** objs, unsigned scalar_sz) {
diff --git a/src/include/lean/object_ref.h b/src/runtime/object_ref.h
similarity index 99%
rename from src/include/lean/object_ref.h
rename to src/runtime/object_ref.h
index 10d0480972..e00a2b95eb 100644
--- a/src/include/lean/object_ref.h
+++ b/src/runtime/object_ref.h
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 #include <algorithm>
 #include <string>
-#include <lean/object.h>
-#include <lean/optional.h>
+#include "runtime/object.h"
+#include "runtime/optional.h"
 
 namespace lean {
 /* Smart point for Lean objects. It is useful for writing C++ code that manipulates Lean objects.  */
diff --git a/src/include/lean/option_ref.h b/src/runtime/option_ref.h
similarity index 98%
rename from src/include/lean/option_ref.h
rename to src/runtime/option_ref.h
index 2c956b7a94..187616e6c9 100644
--- a/src/include/lean/option_ref.h
+++ b/src/runtime/option_ref.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Sebastian Ullrich
 */
 #pragma once
-#include <lean/object_ref.h>
+#include "runtime/object_ref.h"
 
 namespace lean {
 /* Wrapper for manipulating Lean option values in C++ */
diff --git a/src/include/lean/optional.h b/src/runtime/optional.h
similarity index 99%
rename from src/include/lean/optional.h
rename to src/runtime/optional.h
index b97bf51b68..cf3455fc54 100644
--- a/src/include/lean/optional.h
+++ b/src/runtime/optional.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <lean/lean.h>
-#include <lean/debug.h>
+#include "runtime/debug.h"
 
 namespace lean {
 /**
diff --git a/src/include/lean/pair_ref.h b/src/runtime/pair_ref.h
similarity index 97%
rename from src/include/lean/pair_ref.h
rename to src/runtime/pair_ref.h
index a76ccd114a..d20bcc4db6 100644
--- a/src/include/lean/pair_ref.h
+++ b/src/runtime/pair_ref.h
@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/object_ref.h>
+#include "runtime/object_ref.h"
 
 namespace lean {
 /* Wrapper for manipulating Lean pairs in C++ */
diff --git a/src/runtime/platform.cpp b/src/runtime/platform.cpp
index ef2249293e..f92db59142 100644
--- a/src/runtime/platform.cpp
+++ b/src/runtime/platform.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/object.h>
+#include "runtime/object.h"
 
 namespace lean {
 extern "C" obj_res lean_system_platform_nbits(obj_arg) {
diff --git a/src/include/lean/platform.h b/src/runtime/platform.h
similarity index 100%
rename from src/include/lean/platform.h
rename to src/runtime/platform.h
diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp
index e4cd12bbbf..c1a485e98d 100644
--- a/src/runtime/process.cpp
+++ b/src/runtime/process.cpp
@@ -25,13 +25,13 @@ Author: Jared Roesch
 #include <sys/wait.h>
 #endif
 
-#include <lean/object.h>
-#include <lean/io.h>
-#include <lean/array_ref.h>
-#include <lean/string_ref.h>
-#include <lean/option_ref.h>
-#include <lean/pair_ref.h>
-#include <lean/buffer.h>
+#include "runtime/object.h"
+#include "runtime/io.h"
+#include "runtime/array_ref.h"
+#include "runtime/string_ref.h"
+#include "runtime/option_ref.h"
+#include "runtime/pair_ref.h"
+#include "runtime/buffer.h"
 
 namespace lean {
 
diff --git a/src/include/lean/process.h b/src/runtime/process.h
similarity index 100%
rename from src/include/lean/process.h
rename to src/runtime/process.h
diff --git a/src/runtime/sharecommon.cpp b/src/runtime/sharecommon.cpp
index 5a1545c41f..d38c16bba2 100644
--- a/src/runtime/sharecommon.cpp
+++ b/src/runtime/sharecommon.cpp
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include <vector>
-#include <lean/object.h>
-#include <lean/hash.h>
+#include "runtime/object.h"
+#include "runtime/hash.h"
 
 namespace lean {
 
diff --git a/src/include/lean/sstream.h b/src/runtime/sstream.h
similarity index 100%
rename from src/include/lean/sstream.h
rename to src/runtime/sstream.h
diff --git a/src/runtime/stack_overflow.cpp b/src/runtime/stack_overflow.cpp
index 2434e52b88..16ede14b10 100644
--- a/src/runtime/stack_overflow.cpp
+++ b/src/runtime/stack_overflow.cpp
@@ -17,7 +17,7 @@ Port of the corresponding Rust code (see links below).
 #include <cstdio>
 #include <cstdlib>
 #include <cstring>
-#include <lean/stack_overflow.h>
+#include "runtime/stack_overflow.h"
 
 namespace lean {
 // stack guard of the main thread
diff --git a/src/include/lean/stack_overflow.h b/src/runtime/stack_overflow.h
similarity index 100%
rename from src/include/lean/stack_overflow.h
rename to src/runtime/stack_overflow.h
diff --git a/src/runtime/stackinfo.cpp b/src/runtime/stackinfo.cpp
index 459e7504e1..c0c52b361b 100644
--- a/src/runtime/stackinfo.cpp
+++ b/src/runtime/stackinfo.cpp
@@ -6,8 +6,8 @@ Author: Leonardo de Moura
 */
 #include <memory.h>
 #include <iostream>
-#include <lean/thread.h>
-#include <lean/exception.h>
+#include "runtime/thread.h"
+#include "runtime/exception.h"
 
 #if !defined(LEAN_USE_SPLIT_STACK)
 #if defined(LEAN_WINDOWS)
diff --git a/src/include/lean/stackinfo.h b/src/runtime/stackinfo.h
similarity index 100%
rename from src/include/lean/stackinfo.h
rename to src/runtime/stackinfo.h
diff --git a/src/include/lean/string_ref.h b/src/runtime/string_ref.h
similarity index 95%
rename from src/include/lean/string_ref.h
rename to src/runtime/string_ref.h
index 47eed12970..a510ee8375 100644
--- a/src/include/lean/string_ref.h
+++ b/src/runtime/string_ref.h
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
-#include <lean/sstream.h>
-#include <lean/object_ref.h>
-#include <lean/list_ref.h>
+#include "runtime/sstream.h"
+#include "runtime/object_ref.h"
+#include "runtime/list_ref.h"
 namespace lean {
 /* Wrapper for Lean string objects */
 class string_ref : public object_ref {
diff --git a/src/runtime/thread.cpp b/src/runtime/thread.cpp
index 4b5dd20629..e742fe1e41 100644
--- a/src/runtime/thread.cpp
+++ b/src/runtime/thread.cpp
@@ -13,11 +13,11 @@ Author: Leonardo de Moura
 #include <pthread.h>
 #endif
 #include <lean/config.h>
-#include <lean/thread.h>
-#include <lean/interrupt.h>
-#include <lean/exception.h>
-#include <lean/alloc.h>
-#include <lean/stack_overflow.h>
+#include "runtime/thread.h"
+#include "runtime/interrupt.h"
+#include "runtime/exception.h"
+#include "runtime/alloc.h"
+#include "runtime/stack_overflow.h"
 
 #ifndef LEAN_DEFAULT_THREAD_STACK_SIZE
 #define LEAN_DEFAULT_THREAD_STACK_SIZE 8*1024*1024 // 8Mb
diff --git a/src/include/lean/thread.h b/src/runtime/thread.h
similarity index 100%
rename from src/include/lean/thread.h
rename to src/runtime/thread.h
diff --git a/src/runtime/utf8.cpp b/src/runtime/utf8.cpp
index 0d4c89ec63..9c51bedd82 100644
--- a/src/runtime/utf8.cpp
+++ b/src/runtime/utf8.cpp
@@ -6,9 +6,9 @@ Author: Leonardo de Moura
 */
 #include <cstdlib>
 #include <string>
-#include <lean/debug.h>
-#include <lean/optional.h>
-#include <lean/utf8.h>
+#include "runtime/debug.h"
+#include "runtime/optional.h"
+#include "runtime/utf8.h"
 
 namespace lean {
 bool is_utf8_next(unsigned char c) { return (c & 0xC0) == 0x80; }
diff --git a/src/include/lean/utf8.h b/src/runtime/utf8.h
similarity index 98%
rename from src/include/lean/utf8.h
rename to src/runtime/utf8.h
index e92cc47c7c..50e8d6b7e3 100644
--- a/src/include/lean/utf8.h
+++ b/src/runtime/utf8.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <vector>
 #include <string>
-#include <lean/optional.h>
+#include "runtime/optional.h"
 
 namespace lean {
 using uchar = unsigned char;
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index 992ac12998..d99cdaa697 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -13,12 +13,12 @@ Author: Leonardo de Moura
 #include <utility>
 #include <vector>
 #include <set>
-#include <lean/stackinfo.h>
-#include <lean/interrupt.h>
-#include <lean/memory.h>
-#include <lean/thread.h>
-#include <lean/debug.h>
-#include <lean/sstream.h>
+#include "runtime/stackinfo.h"
+#include "runtime/interrupt.h"
+#include "runtime/memory.h"
+#include "runtime/thread.h"
+#include "runtime/debug.h"
+#include "runtime/sstream.h"
 #include "util/timer.h"
 #include "util/macros.h"
 #include "util/io.h"
diff --git a/src/util/bit_tricks.cpp b/src/util/bit_tricks.cpp
index 21ea22a5f0..9ec919f3ca 100644
--- a/src/util/bit_tricks.cpp
+++ b/src/util/bit_tricks.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/debug.h>
+#include "runtime/debug.h"
 
 namespace lean {
 unsigned log2(unsigned v) {
diff --git a/src/util/exception_with_pos.h b/src/util/exception_with_pos.h
index 66be1eda94..ef05d941fc 100644
--- a/src/util/exception_with_pos.h
+++ b/src/util/exception_with_pos.h
@@ -8,7 +8,7 @@ Author: Sebastian Ullrich
 #include <exception>
 #include <string>
 #include <memory>
-#include <lean/exception.h>
+#include "runtime/exception.h"
 #include "util/message_definitions.h"
 
 namespace lean {
diff --git a/src/util/format.cpp b/src/util/format.cpp
index 0991dd2624..692661db5b 100644
--- a/src/util/format.cpp
+++ b/src/util/format.cpp
@@ -10,9 +10,9 @@
 #include <utility>
 #include <vector>
 #include <unordered_map>
-#include <lean/interrupt.h>
-#include <lean/sstream.h>
-#include <lean/hash.h>
+#include "runtime/interrupt.h"
+#include "runtime/sstream.h"
+#include "runtime/hash.h"
 #include "util/options.h"
 #include "util/option_declarations.h"
 #include "util/format.h"
diff --git a/src/util/format.h b/src/util/format.h
index fd6e84ced5..17b274961d 100644
--- a/src/util/format.h
+++ b/src/util/format.h
@@ -12,8 +12,8 @@ Author: Soonho Kong
 #include <utility>
 #include <string>
 #include <vector>
-#include <lean/debug.h>
-#include <lean/object_ref.h>
+#include "runtime/debug.h"
+#include "runtime/object_ref.h"
 #include "util/name.h"
 #include "util/pair.h"
 
diff --git a/src/util/init_module.cpp b/src/util/init_module.cpp
index 0e321accd0..da0a6f9d6d 100644
--- a/src/util/init_module.cpp
+++ b/src/util/init_module.cpp
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/init_module.h>
+#include "runtime/init_module.h"
 #include "util/ascii.h"
 #include "util/name.h"
 #include "util/name_generator.h"
diff --git a/src/util/io.h b/src/util/io.h
index e25d1cd9fc..7fa323471e 100644
--- a/src/util/io.h
+++ b/src/util/io.h
@@ -5,9 +5,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #pragma once
-#include <lean/exception.h>
-#include <lean/object.h>
-#include <lean/string_ref.h>
+#include "runtime/exception.h"
+#include "runtime/object.h"
+#include "runtime/string_ref.h"
 
 namespace lean {
 extern "C" object* lean_io_error_to_string(object * err);
diff --git a/src/util/kvmap.h b/src/util/kvmap.h
index e767ce3d34..2d454bd578 100644
--- a/src/util/kvmap.h
+++ b/src/util/kvmap.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
-#include <lean/pair_ref.h>
+#include "runtime/pair_ref.h"
 #include "util/name.h"
 
 namespace lean {
diff --git a/src/util/list.h b/src/util/list.h
index 456f521a5b..2ba38a989a 100644
--- a/src/util/list.h
+++ b/src/util/list.h
@@ -7,9 +7,9 @@ Author: Leonardo de Moura
 #pragma once
 #include <iostream>
 #include <iterator>
-#include <lean/debug.h>
-#include <lean/optional.h>
-#include <lean/buffer.h>
+#include "runtime/debug.h"
+#include "runtime/optional.h"
+#include "runtime/buffer.h"
 #include "util/rc.h"
 
 namespace lean {
diff --git a/src/util/list_fn.h b/src/util/list_fn.h
index bbab64155e..3389b3c416 100644
--- a/src/util/list_fn.h
+++ b/src/util/list_fn.h
@@ -7,7 +7,7 @@ Author: Leonardo de Moura
 #pragma once
 #include <utility>
 #include <functional>
-#include <lean/buffer.h>
+#include "runtime/buffer.h"
 #include "util/list.h"
 #include "util/pair.h"
 
diff --git a/src/util/map_foreach.h b/src/util/map_foreach.h
index 661afe4242..29c33af891 100644
--- a/src/util/map_foreach.h
+++ b/src/util/map_foreach.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <functional>
-#include <lean/object.h>
+#include "runtime/object.h"
 
 namespace lean {
 /* Helper functions for iterating over Lean maps. */
diff --git a/src/util/message_definitions.h b/src/util/message_definitions.h
index 8b3057fa97..94aa8cf659 100644
--- a/src/util/message_definitions.h
+++ b/src/util/message_definitions.h
@@ -7,7 +7,7 @@ Author: Gabriel Ebner
 #pragma once
 #include <utility>
 #include <string>
-#include <lean/int64.h>
+#include "runtime/int64.h"
 #include "util/name.h"
 
 namespace lean {
diff --git a/src/util/name.cpp b/src/util/name.cpp
index 78f1358604..c196019516 100644
--- a/src/util/name.cpp
+++ b/src/util/name.cpp
@@ -10,12 +10,12 @@ Author: Leonardo de Moura
 #include <algorithm>
 #include <sstream>
 #include <string>
-#include <lean/thread.h>
-#include <lean/debug.h>
-#include <lean/sstream.h>
-#include <lean/utf8.h>
-#include <lean/hash.h>
-#include <lean/buffer.h>
+#include "runtime/thread.h"
+#include "runtime/debug.h"
+#include "runtime/sstream.h"
+#include "runtime/utf8.h"
+#include "runtime/hash.h"
+#include "runtime/buffer.h"
 #include "util/name.h"
 #include "util/ascii.h"
 
diff --git a/src/util/name.h b/src/util/name.h
index 1689455fd5..9c1d70e575 100644
--- a/src/util/name.h
+++ b/src/util/name.h
@@ -10,10 +10,10 @@ Author: Leonardo de Moura
 #include <functional>
 #include <algorithm>
 #include <utility>
-#include <lean/optional.h>
-#include <lean/string_ref.h>
-#include <lean/list_ref.h>
-#include <lean/buffer.h>
+#include "runtime/optional.h"
+#include "runtime/string_ref.h"
+#include "runtime/list_ref.h"
+#include "runtime/buffer.h"
 #include "util/pair.h"
 #include "util/nat.h"
 
diff --git a/src/util/name_generator.cpp b/src/util/name_generator.cpp
index 6c9c6e5337..1ac890b881 100644
--- a/src/util/name_generator.cpp
+++ b/src/util/name_generator.cpp
@@ -5,7 +5,7 @@ Author: Leonardo de Moura
 */
 #include <limits>
 #include <algorithm>
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "util/name_generator.h"
 #include "util/name_set.h"
 
diff --git a/src/util/nat.h b/src/util/nat.h
index 9ea90ee315..e0bae8429a 100644
--- a/src/util/nat.h
+++ b/src/util/nat.h
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #pragma once
 #include <string>
-#include <lean/object_ref.h>
+#include "runtime/object_ref.h"
 
 namespace lean {
 /* Wrapper for manipulating Lean runtime nat values in C++. */
diff --git a/src/util/option_declarations.cpp b/src/util/option_declarations.cpp
index 2fadd0da73..403f5fc2d8 100644
--- a/src/util/option_declarations.cpp
+++ b/src/util/option_declarations.cpp
@@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
-#include <lean/array_ref.h>
-#include <lean/pair_ref.h>
+#include "runtime/array_ref.h"
+#include "runtime/pair_ref.h"
 #include "util/option_declarations.h"
 #include "util/io.h"
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index c8d9ac6c28..365448881a 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include <memory>
 #include <string>
-#include <lean/sstream.h>
+#include "runtime/sstream.h"
 #include "util/options.h"
 #include "util/option_declarations.h"
 
diff --git a/src/util/path.cpp b/src/util/path.cpp
index 45c1ddcfe7..0bfe6d9631 100644
--- a/src/util/path.cpp
+++ b/src/util/path.cpp
@@ -15,9 +15,9 @@ Author: Leonardo de Moura, Gabriel Ebner
 #include <vector>
 #include <sys/types.h>
 #include <sys/stat.h>
-#include <lean/exception.h>
-#include <lean/sstream.h>
-#include <lean/optional.h>
+#include "runtime/exception.h"
+#include "runtime/sstream.h"
+#include "runtime/optional.h"
 
 #ifdef _MSC_VER
 #define S_ISDIR(mode) ((mode & _S_IFDIR) != 0)
diff --git a/src/util/path.h b/src/util/path.h
index d90572d8d2..8170fe767c 100644
--- a/src/util/path.h
+++ b/src/util/path.h
@@ -8,8 +8,8 @@ Author: Leonardo de Moura, Gabriel Ebner
 #include <string>
 #include <vector>
 #include <ios>
-#include <lean/exception.h>
-#include <lean/optional.h>
+#include "runtime/exception.h"
+#include "runtime/optional.h"
 
 namespace lean {
 class file_not_found_exception : public exception {
diff --git a/src/util/rb_tree.h b/src/util/rb_tree.h
index 5515981ef7..b6e4733ec5 100644
--- a/src/util/rb_tree.h
+++ b/src/util/rb_tree.h
@@ -12,9 +12,9 @@ Author: Leonardo de Moura
 #endif
 #include <utility>
 #include <algorithm>
-#include <lean/optional.h>
-#include <lean/debug.h>
-#include <lean/buffer.h>
+#include "runtime/optional.h"
+#include "runtime/debug.h"
+#include "runtime/buffer.h"
 #include "util/rc.h"
 
 
diff --git a/src/util/rc.h b/src/util/rc.h
index 168fd4aae4..bc33348f34 100644
--- a/src/util/rc.h
+++ b/src/util/rc.h
@@ -7,8 +7,8 @@ Author: Leonardo de Moura
 #pragma once
 
 // Goodies for reference counting
-#include <lean/thread.h>
-#include <lean/debug.h>
+#include "runtime/thread.h"
+#include "runtime/debug.h"
 
 #define MK_LEAN_RC()                                                    \
 private:                                                                \
diff --git a/src/util/test.h b/src/util/test.h
index 00edd8b0e9..bd5a3b07e3 100644
--- a/src/util/test.h
+++ b/src/util/test.h
@@ -9,5 +9,5 @@ Author: Leonardo de Moura
 #ifndef LEAN_DEBUG
 #define LEAN_DEBUG
 #endif
-#include <lean/debug.h>
-#include <lean/stackinfo.h>
+#include "runtime/debug.h"
+#include "runtime/stackinfo.h"
diff --git a/src/util/timer.h b/src/util/timer.h
index 74c8de9eb2..bffa7be1e5 100644
--- a/src/util/timer.h
+++ b/src/util/timer.h
@@ -5,8 +5,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Gabriel Ebner
 */
 #pragma once
-#include <lean/thread.h>
-#include <lean/optional.h>
+#include "runtime/thread.h"
+#include "runtime/optional.h"
 
 namespace lean {