From da481c327416bd0038e0dd8ac45716a74b785eea Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 23 Sep 2014 12:09:13 -0700
Subject: [PATCH] refactor(kernel): explicit initialization/finalization

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 src/frontends/lean/pp.cpp            |  2 +-
 src/frontends/lean/structure_cmd.cpp |  2 +-
 src/kernel/converter.cpp             | 26 +++++++++++++-----
 src/kernel/converter.h               |  3 +++
 src/kernel/declaration.cpp           | 12 +++++++--
 src/kernel/declaration.h             |  3 +++
 src/kernel/expr.cpp                  | 40 +++++++++++++++-------------
 src/kernel/expr.h                    |  5 ++--
 src/kernel/formatter.cpp             | 13 +++++++--
 src/kernel/formatter.h               |  3 +++
 src/kernel/init_module.cpp           | 19 +++++++++++++
 src/kernel/level.cpp                 | 32 +++++++++++-----------
 src/kernel/level.h                   |  3 +++
 src/kernel/type_checker.cpp          | 18 ++++++++-----
 src/kernel/type_checker.h            |  3 +++
 src/library/kernel_bindings.cpp      |  4 +--
 src/tests/kernel/environment.cpp     |  5 ++++
 src/tests/kernel/expr.cpp            |  9 +++++++
 src/tests/kernel/free_vars.cpp       | 11 +++++++-
 src/tests/kernel/instantiate.cpp     | 10 +++++++
 src/tests/kernel/max_sharing.cpp     | 12 +++++++++
 src/tests/kernel/metavar.cpp         | 16 +++++++++++
 src/tests/kernel/replace.cpp         | 11 ++++++++
 src/tests/library/deep_copy.cpp      | 13 +++++++++
 src/tests/library/head_map.cpp       | 13 +++++++++
 src/tests/library/occurs.cpp         | 13 +++++++++
 src/tests/library/unifier.cpp        |  1 +
 27 files changed, 243 insertions(+), 59 deletions(-)

diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp
index fd7ee0f59..5aa218e3c 100644
--- a/src/frontends/lean/pp.cpp
+++ b/src/frontends/lean/pp.cpp
@@ -261,7 +261,7 @@ auto pretty_fn::pp_var(expr const & e) -> result {
 }
 
 auto pretty_fn::pp_sort(expr const & e) -> result {
-    if (m_env.impredicative() && e == Prop) {
+    if (m_env.impredicative() && e == mk_Prop()) {
         return mk_result(format("Prop"));
     } else if (m_universes) {
         return mk_result(group(format("Type.{") + nest(6, pp_level(sort_level(e))) + format("}")));
diff --git a/src/frontends/lean/structure_cmd.cpp b/src/frontends/lean/structure_cmd.cpp
index f7566a319..abd6a7cb0 100644
--- a/src/frontends/lean/structure_cmd.cpp
+++ b/src/frontends/lean/structure_cmd.cpp
@@ -141,7 +141,7 @@ struct structure_cmd_fn {
     /** \brief Collect section local parameters used in m_params and m_fields */
     void collect_section_locals(expr_struct_set & ls) {
         collect_locals(m_type, ls);
-        expr tmp = Pi(m_fields, Prop, m_p); // temp expr just for collecting section parameters occurring in the fields.
+        expr tmp = Pi(m_fields, mk_Prop(), m_p); // temp expr just for collecting section parameters occurring in the fields.
         collect_locals(tmp, ls);
     }
 
diff --git a/src/kernel/converter.cpp b/src/kernel/converter.cpp
index bc7b4b43d..a3bbd90b4 100644
--- a/src/kernel/converter.cpp
+++ b/src/kernel/converter.cpp
@@ -67,9 +67,9 @@ optional<declaration> is_delta(environment const & env, expr const & e,
     return is_delta_core(env, get_app_fn(e), pred, mod_idx);
 }
 
-static optional<module_idx> g_opt_main_module_idx(g_main_module_idx);
+static optional<module_idx> * g_opt_main_module_idx = nullptr;
 optional<declaration> is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred) {
-    return is_delta(env, e, pred, g_opt_main_module_idx);
+    return is_delta(env, e, pred, *g_opt_main_module_idx);
 }
 
 optional<declaration> is_delta(environment const & env, expr const & e) {
@@ -77,9 +77,9 @@ optional<declaration> is_delta(environment const & env, expr const & e) {
 }
 
 
-static no_delayed_justification g_no_delayed_jst;
+static no_delayed_justification * g_no_delayed_jst = nullptr;
 pair<bool, constraint_seq> converter::is_def_eq(expr const & t, expr const & s, type_checker & c) {
-    return is_def_eq(t, s, c, g_no_delayed_jst);
+    return is_def_eq(t, s, c, *g_no_delayed_jst);
 }
 
 /** \brief Do nothing converter */
@@ -100,7 +100,7 @@ std::unique_ptr<converter> mk_dummy_converter() {
 name converter::mk_fresh_name(type_checker & tc) { return tc.mk_fresh_name(); }
 pair<expr, constraint_seq> converter::infer_type(type_checker & tc, expr const & e) { return tc.infer_type(e); }
 extension_context & converter::get_extension(type_checker & tc) { return tc.get_extension(); }
-static expr g_dont_care(Const("dontcare"));
+static expr * g_dont_care = nullptr;
 
 struct default_converter : public converter {
     environment                                 m_env;
@@ -355,7 +355,7 @@ struct default_converter : public converter {
                     var_s_type = instantiate_rev(binding_domain(s), subst.size(), subst.data());
                 subst.push_back(mk_local(mk_fresh_name(c), binding_name(s), *var_s_type, binding_info(s)));
             } else {
-                subst.push_back(g_dont_care); // don't care
+                subst.push_back(*g_dont_care); // don't care
             }
             t = binding_body(t);
             s = binding_body(s);
@@ -618,7 +618,7 @@ struct default_converter : public converter {
     pair<bool, constraint_seq> is_prop(expr const & e, type_checker & c) {
         auto tcs = infer_type(c, e);
         auto wcs = whnf(tcs.first, c);
-        if (wcs.first == Prop)
+        if (wcs.first == mk_Prop())
             return to_bcs(true, wcs.second + tcs.second);
         else
             return to_bcs(false);
@@ -647,4 +647,16 @@ std::unique_ptr<converter> mk_default_converter(environment const & env, bool un
 std::unique_ptr<converter> mk_default_converter(environment const & env, bool unfold_opaque_main, bool memoize) {
     return mk_default_converter(env, unfold_opaque_main, memoize, g_always_false);
 }
+
+void initialize_converter() {
+    g_opt_main_module_idx = new optional<module_idx>(g_main_module_idx);
+    g_no_delayed_jst      = new no_delayed_justification();
+    g_dont_care           = new expr(Const("dontcare"));
+}
+
+void finalize_converter() {
+    delete g_opt_main_module_idx;
+    delete g_no_delayed_jst;
+    delete g_dont_care;
+}
 }
diff --git a/src/kernel/converter.h b/src/kernel/converter.h
index 194d9e2d7..c02515f91 100644
--- a/src/kernel/converter.h
+++ b/src/kernel/converter.h
@@ -38,4 +38,7 @@ bool is_opaque(declaration const & d, extra_opaque_pred const & pred, optional<m
 optional<declaration> is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred, optional<module_idx> const & mod_idx);
 optional<declaration> is_delta(environment const & env, expr const & e, extra_opaque_pred const & pred);
 optional<declaration> is_delta(environment const & env, expr const & e);
+
+void initialize_converter();
+void finalize_converter();
 }
diff --git a/src/kernel/declaration.cpp b/src/kernel/declaration.cpp
index 47197cd18..9045f8339 100644
--- a/src/kernel/declaration.cpp
+++ b/src/kernel/declaration.cpp
@@ -38,9 +38,9 @@ struct declaration::cell {
         m_value(v), m_weight(w), m_module_idx(mod_idx), m_opaque(opaque), m_use_conv_opt(use_conv_opt) {}
 };
 
-declaration g_dummy = mk_axiom(name(), level_param_names(), expr());
+static declaration * g_dummy = nullptr;
 
-declaration::declaration():declaration(g_dummy) {}
+declaration::declaration():declaration(*g_dummy) {}
 declaration::declaration(cell * ptr):m_ptr(ptr) {}
 declaration::declaration(declaration const & s):m_ptr(s.m_ptr) { if (m_ptr) m_ptr->inc_ref(); }
 declaration::declaration(declaration && s):m_ptr(s.m_ptr) { s.m_ptr = nullptr; }
@@ -90,4 +90,12 @@ declaration mk_axiom(name const & n, level_param_names const & params, expr cons
 declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t) {
     return declaration(new declaration::cell(n, params, t, false));
 }
+
+void initialize_declaration() {
+    g_dummy = new declaration(mk_axiom(name(), level_param_names(), expr()));
+}
+
+void finalize_declaration() {
+    delete g_dummy;
+}
 }
diff --git a/src/kernel/declaration.h b/src/kernel/declaration.h
index 51d67ddcb..5e988f0d6 100644
--- a/src/kernel/declaration.h
+++ b/src/kernel/declaration.h
@@ -89,4 +89,7 @@ declaration mk_definition(environment const & env, name const & n, level_param_n
 declaration mk_theorem(name const & n, level_param_names const & params, expr const & t, expr const & v, module_idx mod_idx = 0);
 declaration mk_axiom(name const & n, level_param_names const & params, expr const & t);
 declaration mk_var_decl(name const & n, level_param_names const & params, expr const & t);
+
+void initialize_declaration();
+void finalize_declaration();
 }
diff --git a/src/kernel/expr.cpp b/src/kernel/expr.cpp
index 6c8f1b6e3..4b93202e6 100644
--- a/src/kernel/expr.cpp
+++ b/src/kernel/expr.cpp
@@ -40,8 +40,8 @@ unsigned inc_weight(unsigned w) {
         return w;
 }
 
-static expr g_dummy(mk_var(0));
-expr::expr():expr(g_dummy) {}
+static expr * g_dummy = nullptr;
+expr::expr():expr(*g_dummy) {}
 
 unsigned hash_levels(levels const & ls) {
     unsigned r = 23;
@@ -448,9 +448,9 @@ unsigned get_app_num_args(expr const & e) {
     return n;
 }
 
+static name * g_default_name = nullptr;
 static name const & get_default_var_name() {
-    static name r("a");
-    return r;
+    return *g_default_name;
 }
 static name const & g_default_var_name = get_default_var_name(); // force it to be initialized
 
@@ -467,20 +467,10 @@ expr mk_pi(unsigned sz, expr const * domain, expr const & range) {
     return r;
 }
 
-expr mk_Prop() {
-    static optional<expr> Prop;
-    if (!Prop) Prop = mk_sort(mk_level_zero());
-    return *Prop;
-}
-
-expr mk_Type() {
-    static optional<expr> Type;
-    if (!Type) Type = mk_sort(mk_level_one());
-    return *Type;
-}
-
-expr Prop = mk_Prop();
-expr Type = mk_Type();
+static expr * g_Prop  = nullptr;
+static expr * g_Type1 = nullptr;
+expr mk_Prop() { return *g_Prop; }
+expr mk_Type() { return *g_Type1; }
 
 unsigned get_weight(expr const & e) {
     switch (e.kind()) {
@@ -653,4 +643,18 @@ expr infer_implicit(expr const & t, unsigned num_params, bool strict) {
 expr infer_implicit(expr const & t, bool strict) {
     return infer_implicit(t, std::numeric_limits<unsigned>::max(), strict);
 }
+
+void initialize_expr() {
+    g_dummy        = new expr(mk_var(0));
+    g_default_name = new name("a");
+    g_Type1        = new expr(mk_sort(mk_level_one()));
+    g_Prop         = new expr(mk_sort(mk_level_zero()));
+}
+
+void finalize_expr() {
+    delete g_Prop;
+    delete g_Type1;
+    delete g_dummy;
+    delete g_default_name;
+}
 }
diff --git a/src/kernel/expr.h b/src/kernel/expr.h
index 0a058a259..ff3aecf80 100644
--- a/src/kernel/expr.h
+++ b/src/kernel/expr.h
@@ -464,8 +464,6 @@ inline expr mk_pi(buffer<expr> const & domain, expr const & range) { return mk_p
 
 expr mk_Prop();
 expr mk_Type();
-extern expr Type;
-extern expr Prop;
 
 bool is_default_var_name(name const & n);
 expr mk_arrow(expr const & t, expr const & e);
@@ -695,4 +693,7 @@ expr infer_implicit(expr const & t, bool strict);
 // =======================================
 
 std::ostream & operator<<(std::ostream & out, expr const & e);
+
+void initialize_expr();
+void finalize_expr();
 }
diff --git a/src/kernel/formatter.cpp b/src/kernel/formatter.cpp
index efaaf93fb..a7a10df5a 100644
--- a/src/kernel/formatter.cpp
+++ b/src/kernel/formatter.cpp
@@ -8,10 +8,12 @@ Author: Leonardo de Moura
 #include "kernel/formatter.h"
 
 namespace lean {
-static std::unique_ptr<std::function<void(std::ostream &, expr const & e)>> g_print;
+static std::function<void(std::ostream &, expr const & e)> * g_print = nullptr;
 
 void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn) {
-    g_print.reset(new std::function<void(std::ostream &, expr const &)>(fn));
+    if (g_print)
+        delete g_print;
+    g_print = new std::function<void(std::ostream &, expr const &)>(fn);
 }
 
 std::ostream & operator<<(std::ostream & out, expr const & e) {
@@ -24,4 +26,11 @@ std::ostream & operator<<(std::ostream & out, expr const & e) {
 }
 
 void print(lean::expr const & a) { std::cout << a << std::endl; }
+
+void initialize_formatter() {}
+
+void finalize_formatter() {
+    if (g_print)
+        delete g_print;
+}
 }
diff --git a/src/kernel/formatter.h b/src/kernel/formatter.h
index d57134092..f0fdba7c3 100644
--- a/src/kernel/formatter.h
+++ b/src/kernel/formatter.h
@@ -30,4 +30,7 @@ std::ostream & operator<<(std::ostream & out, expr const & e);
 typedef std::function<format(formatter const &)> pp_fn;
 
 void set_print_fn(std::function<void(std::ostream &, expr const &)> const & fn);
+
+void initialize_formatter();
+void finalize_formatter();
 }
diff --git a/src/kernel/init_module.cpp b/src/kernel/init_module.cpp
index 510288c0f..728ecfd1d 100644
--- a/src/kernel/init_module.cpp
+++ b/src/kernel/init_module.cpp
@@ -5,11 +5,30 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
+#include "kernel/converter.h"
+#include "kernel/type_checker.h"
+#include "kernel/expr.h"
+#include "kernel/formatter.h"
+#include "kernel/level.h"
+#include "kernel/declaration.h"
+
 namespace lean {
 void initialize_kernel_module() {
+    initialize_level();
+    initialize_expr();
+    initialize_declaration();
+    initialize_converter();
+    initialize_type_checker();
     initialize_environment();
+    initialize_formatter();
 }
 void finalize_kernel_module() {
+    finalize_formatter();
     finalize_environment();
+    finalize_type_checker();
+    finalize_converter();
+    finalize_declaration();
+    finalize_expr();
+    finalize_level();
 }
 }
diff --git a/src/kernel/level.cpp b/src/kernel/level.cpp
index 7c12fdb03..36f2599e1 100644
--- a/src/kernel/level.cpp
+++ b/src/kernel/level.cpp
@@ -241,23 +241,11 @@ level mk_param_univ(name const & n) { return level(new level_param_core(level_ki
 level mk_global_univ(name const & n) { return level(new level_param_core(level_kind::Global, n)); }
 level mk_meta_univ(name const & n) { return level(new level_param_core(level_kind::Meta, n)); }
 
-level const & mk_level_zero() {
-    static optional<level> r;
-    if (!r) r = level(new level_cell(level_kind::Zero, 7u));
-    return *r;
-}
-level const & mk_level_one() {
-    static optional<level> r;
-    if (!r) r = mk_succ(mk_level_zero());
-    return *r;
-}
-// Force g_one_ptr and g_zero_ptr to be created at initialization time.
-// Purpose: avoid any kind of synchronization at mk_level_zero and mk_level_one
-static level g_dummy(mk_level_one());
-
-bool is_one(level const & l) {
-    return l == mk_level_one();
-}
+static level * g_level_zero = nullptr;
+static level * g_level_one  = nullptr;
+level const & mk_level_zero() { return *g_level_zero; }
+level const & mk_level_one() { return *g_level_one; }
+bool is_one(level const & l) { return l == mk_level_one(); }
 
 level::level():level(mk_level_zero()) {}
 level::level(level_cell * ptr):m_ptr(ptr) { if (m_ptr) m_ptr->inc_ref(); }
@@ -712,5 +700,15 @@ bool is_geq(level const & l1, level const & l2) {
 levels param_names_to_levels(level_param_names const & ps) {
     return map2<level>(ps, [](name const & p) { return mk_param_univ(p); });
 }
+
+void initialize_level() {
+    g_level_zero = new level(new level_cell(level_kind::Zero, 7u));
+    g_level_one  = new level(mk_succ(mk_level_zero()));
+}
+
+void finalize_level() {
+    delete g_level_one;
+    delete g_level_zero;
+}
 }
 void print(lean::level const & l) { std::cout << l << std::endl; }
diff --git a/src/kernel/level.h b/src/kernel/level.h
index bd3013824..35a347e82 100644
--- a/src/kernel/level.h
+++ b/src/kernel/level.h
@@ -221,5 +221,8 @@ format pp(level const & lhs, level const & rhs, bool unicode, unsigned indent);
 format pp(level const & lhs, level const & rhs, options const & opts = options());
 /** \brief Convert a list of universe level parameter names into a list of levels. */
 levels param_names_to_levels(level_param_names const & ps);
+
+void initialize_level();
+void finalize_level();
 }
 void print(lean::level const & l);
diff --git a/src/kernel/type_checker.cpp b/src/kernel/type_checker.cpp
index f7f76be9c..50270c4fc 100644
--- a/src/kernel/type_checker.cpp
+++ b/src/kernel/type_checker.cpp
@@ -22,8 +22,6 @@ Author: Leonardo de Moura
 #include "kernel/replace_fn.h"
 
 namespace lean {
-static name g_x_name("x");
-
 expr replace_range(expr const & type, expr const & new_range) {
     if (is_pi(type))
         return update_binding(type, binding_domain(type), replace_range(binding_body(type), new_range));
@@ -398,7 +396,7 @@ pair<bool, constraint_seq> type_checker::is_def_eq_types(expr const & t, expr co
 pair<bool, constraint_seq> type_checker::is_prop(expr const & e) {
     auto tcs  = infer_type(e);
     auto wtcs = whnf(tcs.first);
-    bool r    = wtcs.first == Prop;
+    bool r    = wtcs.first == mk_Prop();
     if (r)
         return mk_pair(true, tcs.second + wtcs.second);
     else
@@ -414,10 +412,10 @@ type_checker::type_checker(environment const & env, name_generator const & g, st
     m_memoize(memoize), m_params(nullptr) {
 }
 
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
 
 type_checker::type_checker(environment const & env):
-    type_checker(env, name_generator(g_tmp_prefix), mk_default_converter(env), true) {}
+    type_checker(env, name_generator(*g_tmp_prefix), mk_default_converter(env), true) {}
 
 type_checker::~type_checker() {}
 
@@ -484,10 +482,18 @@ certified_declaration check(environment const & env, declaration const & d, name
 }
 
 certified_declaration check(environment const & env, declaration const & d, extra_opaque_pred const & pred) {
-    return check(env, d, name_generator(g_tmp_prefix), pred);
+    return check(env, d, name_generator(*g_tmp_prefix), pred);
 }
 
 certified_declaration check(environment const & env, declaration const & d) {
     return check(env, d, no_extra_opaque());
 }
+
+void initialize_type_checker() {
+    g_tmp_prefix = new name(name::mk_internal_unique_name());
+}
+
+void finalize_type_checker() {
+    delete g_tmp_prefix;
+}
 }
diff --git a/src/kernel/type_checker.h b/src/kernel/type_checker.h
index 20e847a35..bc56ac9ee 100644
--- a/src/kernel/type_checker.h
+++ b/src/kernel/type_checker.h
@@ -235,4 +235,7 @@ public:
     app_delayed_justification(expr const & e, expr const & arg, expr const & f_type, expr const & a_type);
     virtual justification get();
 };
+
+void initialize_type_checker();
+void finalize_type_checker();
 }
diff --git a/src/library/kernel_bindings.cpp b/src/library/kernel_bindings.cpp
index 09461b932..211e9f1da 100644
--- a/src/library/kernel_bindings.cpp
+++ b/src/library/kernel_bindings.cpp
@@ -686,10 +686,10 @@ static void open_expr(lua_State * L) {
 
     SET_GLOBAL_FUN(enable_expr_caching, "enable_expr_caching");
 
-    push_expr(L, Prop);
+    push_expr(L, mk_Prop());
     lua_setglobal(L, "Prop");
 
-    push_expr(L, Type);
+    push_expr(L, mk_Type());
     lua_setglobal(L, "Type");
 
     lua_newtable(L);
diff --git a/src/tests/kernel/environment.cpp b/src/tests/kernel/environment.cpp
index e536b8493..f45884114 100644
--- a/src/tests/kernel/environment.cpp
+++ b/src/tests/kernel/environment.cpp
@@ -64,11 +64,13 @@ static void tst1() {
     } catch (kernel_exception & ex) {
         std::cout << "expected error: " << ex.pp(mk_formatter(ex.get_environment())) << "\n";
     }
+    expr Type = mk_Type();
     expr A = Local("A", Type);
     expr x = Local("x", A);
     auto env3 = add_decl(env2, mk_definition("id", level_param_names(),
                                              Pi(A, A >> A),
                                              Fun({A, x}, x)));
+    expr Prop = mk_Prop();
     expr c  = mk_local("c", Prop);
     expr id = Const("id");
     type_checker checker(env3, name_generator("tmp"));
@@ -83,6 +85,7 @@ static void tst1() {
 static void tst2() {
     environment env;
     name base("base");
+    expr Prop = mk_Prop();
     env = add_decl(env, mk_var_decl(name(base, 0u), level_param_names(), Prop >> (Prop >> Prop)));
     expr x = Local("x", Prop);
     expr y = Local("y", Prop);
@@ -91,6 +94,7 @@ static void tst2() {
         env = add_decl(env, mk_definition(env, name(base, i), level_param_names(), Prop >> (Prop >> Prop),
                                           Fun({x, y}, prev(prev(x, y), prev(y, x)))));
     }
+    expr Type = mk_Type();
     expr A = Local("A", Type);
     expr a = Local("a", A);
     env = add_decl(env, mk_definition("id", level_param_names(),
@@ -136,6 +140,7 @@ public:
 
 static void tst3() {
     environment env(0, true, true, true, std::unique_ptr<normalizer_extension>(new normalizer_extension_tst()));
+    expr Type = mk_Type();
     expr A = Local("A", Type);
     expr x = Local("x", A);
     expr id = Const("id");
diff --git a/src/tests/kernel/expr.cpp b/src/tests/kernel/expr.cpp
index 7fbfaa1c7..4e81ef1b9 100644
--- a/src/tests/kernel/expr.cpp
+++ b/src/tests/kernel/expr.cpp
@@ -45,6 +45,7 @@ static void tst1() {
     expr f;
     f = Var(0);
     expr fa = f(a);
+    expr Type = mk_Type();
     expr ty = Type;
     std::cout << fa << "\n";
     std::cout << fa(a) << "\n";
@@ -181,6 +182,7 @@ static void tst8() {
     expr x = Var(0);
     expr a = Const("a");
     expr n = Const("n");
+    expr Type = mk_Type();
     expr p = Type;
     expr y = Var(1);
     lean_assert(closed(a));
@@ -239,6 +241,7 @@ static void tst11() {
     expr b = Const("b");
     expr x = Var(0);
     expr y = Var(1);
+    expr Type = mk_Type();
     expr t = Type;
     std::cout << instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) << "\n";
     lean_assert(instantiate(mk_lambda("x", t, f(f(y, b), f(x, y))), f(a)) ==
@@ -263,6 +266,7 @@ static void tst12() {
 }
 
 static void tst13() {
+    expr Type = mk_Type();
     expr t0 = Type;
     expr t1 = mk_sort(mk_succ(mk_succ(level())));
     check_serializer(t0);
@@ -282,7 +286,9 @@ static void tst14() {
 static void tst15() {
     expr f = Const("f");
     expr x = Var(0);
+    expr Type = mk_Type();
     expr a = Local("a", Type);
+    expr Prop = mk_Prop();
     expr m = mk_metavar("m", Prop);
     check_serializer(m);
     lean_assert(has_metavar(m));
@@ -314,6 +320,7 @@ static void tst16() {
     expr f = Const("f");
     expr a = Const("a");
     check_copy(f(a));
+    expr Prop = mk_Prop();
     check_copy(mk_metavar("M", Prop));
     check_copy(mk_lambda("x", a, Var(0)));
     check_copy(mk_pi("x", a, Var(0)));
@@ -338,9 +345,11 @@ static void tst17() {
 static void tst18() {
     expr f = Const("f");
     expr x = Var(0);
+    expr Prop = mk_Prop();
     expr l = mk_local("m", Prop);
     expr m = mk_metavar("m", Prop);
     expr a0 = Const("a");
+    expr Type = mk_Type();
     expr a  = Local("a", Type);
     expr a1 = Local("a", m);
     expr a2 = Local("a", l);
diff --git a/src/tests/kernel/free_vars.cpp b/src/tests/kernel/free_vars.cpp
index 1b4d7e34c..b44da773d 100644
--- a/src/tests/kernel/free_vars.cpp
+++ b/src/tests/kernel/free_vars.cpp
@@ -5,8 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/free_vars.h"
 #include "kernel/abstract.h"
+#include "kernel/init_module.h"
 using namespace lean;
 
 static void tst1() {
@@ -59,7 +62,7 @@ static void tst3() {
 
 static void tst4() {
     expr f = Const("f");
-    expr B = Prop;
+    expr B = mk_Prop();
     expr x = Local("x", B);
     expr y = Local("y", B);
     expr t = f(Fun({x, y}, f(x, y))(f(Var(1), Var(2))), x);
@@ -72,9 +75,15 @@ static void tst4() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
     tst1();
     tst2();
     tst3();
     tst4();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/kernel/instantiate.cpp b/src/tests/kernel/instantiate.cpp
index fe95e9e3d..7ed456265 100644
--- a/src/tests/kernel/instantiate.cpp
+++ b/src/tests/kernel/instantiate.cpp
@@ -5,8 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 using namespace lean;
 
 static void tst1() {
@@ -33,6 +37,12 @@ static void tst1() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
     tst1();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/kernel/max_sharing.cpp b/src/tests/kernel/max_sharing.cpp
index b8eb1f8e2..e6cbb5fb7 100644
--- a/src/tests/kernel/max_sharing.cpp
+++ b/src/tests/kernel/max_sharing.cpp
@@ -6,7 +6,11 @@ Author: Leonardo de Moura
 */
 #include <iostream>
 #include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/abstract.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 #include "library/max_sharing.h"
 #include "library/print.h"
 using namespace lean;
@@ -60,10 +64,18 @@ static void tst3() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_module();
     init_default_print_fn();
     scoped_expr_caching set(false);
     tst1();
     tst2();
     tst3();
+    finalize_library_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/kernel/metavar.cpp b/src/tests/kernel/metavar.cpp
index 9bc0b2348..2f20c287b 100644
--- a/src/tests/kernel/metavar.cpp
+++ b/src/tests/kernel/metavar.cpp
@@ -11,9 +11,13 @@ Author: Leonardo de Moura
 #include <set>
 #include "util/test.h"
 #include "util/buffer.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/metavar.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 #include "library/print.h"
 using namespace lean;
 
@@ -69,6 +73,7 @@ static bool check_assumptions(justification const & j, std::initializer_list<uns
 
 static void tst1() {
     substitution subst;
+    expr Prop = mk_Prop();
     expr m1 = mk_metavar("m1", Prop);
     lean_assert(!subst.is_assigned(m1));
     expr m2 = mk_metavar("m2", Prop);
@@ -86,6 +91,7 @@ static void tst1() {
 
 static void tst2() {
     substitution s;
+    expr Prop = mk_Prop();
     expr m1 = mk_metavar("m1", Prop);
     expr m2 = mk_metavar("m2", Prop);
     expr m3 = mk_metavar("m3", Prop);
@@ -108,6 +114,7 @@ static void tst2() {
 }
 
 static void tst3() {
+    expr Prop = mk_Prop();
     expr m1 = mk_metavar("m1", Prop >> (Prop >> Prop));
     substitution s;
     expr f  = Const("f");
@@ -124,6 +131,7 @@ static void tst3() {
 }
 
 static void tst4() {
+    expr Prop = mk_Prop();
     expr m1  = mk_metavar("m1", Prop);
     expr m2  = mk_metavar("m2", Prop);
     expr m3  = mk_metavar("m3", Prop);
@@ -146,10 +154,18 @@ static void tst4() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_module();
     init_default_print_fn();
     tst1();
     tst2();
     tst3();
     tst4();
+    finalize_library_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/kernel/replace.cpp b/src/tests/kernel/replace.cpp
index 7ab5ccad2..3aba1521d 100644
--- a/src/tests/kernel/replace.cpp
+++ b/src/tests/kernel/replace.cpp
@@ -6,11 +6,15 @@ Author: Leonardo de Moura
 */
 #include "util/test.h"
 #include "util/name.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/expr.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/expr_maps.h"
 #include "kernel/replace_fn.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 #include "library/print.h"
 using namespace lean;
 
@@ -31,6 +35,7 @@ static void tst1() {
 }
 
 static void tst2() {
+    expr Type = mk_Type();
     expr r = mk_lambda("x", Type, mk_app({Var(0), Var(1), Var(2)}));
     std::cout << instantiate(r, Const("a")) << std::endl;
     lean_assert(instantiate(r, Const("a")) == mk_lambda("x", Type, mk_app({Var(0), Const("a"), Var(1)})));
@@ -60,8 +65,14 @@ public:
 int main() {
     save_stack_info();
     init_default_print_fn();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
     tst1();
     tst2();
     std::cout << "done" << "\n";
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/library/deep_copy.cpp b/src/tests/library/deep_copy.cpp
index 90ccbe741..d8c0217a8 100644
--- a/src/tests/library/deep_copy.cpp
+++ b/src/tests/library/deep_copy.cpp
@@ -5,8 +5,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 #include "library/deep_copy.h"
 using namespace lean;
 
@@ -14,6 +18,7 @@ static void tst1() {
     expr f = Const("f");
     expr a = Const("a");
     expr x = Var(0);
+    expr Type = mk_Type();
     expr t = Type;
     expr z = Const("z");
     expr m = mk_metavar("a", Type);
@@ -25,6 +30,14 @@ static void tst1() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_module();
     tst1();
+    finalize_library_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/library/head_map.cpp b/src/tests/library/head_map.cpp
index 18bbaccc3..dd6be7d34 100644
--- a/src/tests/library/head_map.cpp
+++ b/src/tests/library/head_map.cpp
@@ -5,7 +5,11 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/abstract.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 #include "library/head_map.h"
 using namespace lean;
 
@@ -14,6 +18,7 @@ static void tst1() {
     expr a = Const("a");
     expr f = Const("f");
     expr b = Const("b");
+    expr Prop = mk_Prop();
     expr x = Local("x", Prop);
     expr l1 = Fun(x, x);
     expr l2 = Fun(x, f(x));
@@ -54,6 +59,14 @@ static void tst1() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_module();
     tst1();
+    finalize_library_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/library/occurs.cpp b/src/tests/library/occurs.cpp
index 873b986a2..66a21b026 100644
--- a/src/tests/library/occurs.cpp
+++ b/src/tests/library/occurs.cpp
@@ -5,14 +5,19 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "util/test.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/abstract.h"
 #include "library/occurs.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 using namespace lean;
 
 static void tst1() {
     expr f = Const("f");
     expr a = Const("a");
     expr b = Const("b");
+    expr Type = mk_Type();
     expr T = Type;
     expr a1 = Local("a", T);
     lean_assert(occurs(f, f));
@@ -25,6 +30,14 @@ static void tst1() {
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_module();
     tst1();
+    finalize_library_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }
diff --git a/src/tests/library/unifier.cpp b/src/tests/library/unifier.cpp
index b1a3d0539..1c6bf0a18 100644
--- a/src/tests/library/unifier.cpp
+++ b/src/tests/library/unifier.cpp
@@ -15,6 +15,7 @@ using namespace lean;
 static void tst1() {
     environment env;
     name_generator ngen("foo");
+    expr Type = mk_Type();
     expr A  = Local("A", Type);
     expr f  = Local("f", A >> (A >> A));
     expr a  = Local("a", A);