refactor(*): explicit initialization/finalization for environment extensions

src/frontends/lean/CMakeLists.txt

@@ -1,12 +1,12 @@
-add_library(lean_frontend register_module.cpp token_table.cpp
+add_library(lean_frontend tokens.cpp register_module.cpp
-scanner.cpp parse_table.cpp parser_config.cpp parser.cpp
+token_table.cpp scanner.cpp parse_table.cpp parser_config.cpp
-parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
+parser.cpp parser_pos_provider.cpp builtin_cmds.cpp builtin_exprs.cpp
-server.cpp notation_cmd.cpp calc.cpp
+server.cpp notation_cmd.cpp calc.cpp decl_cmds.cpp util.cpp
-decl_cmds.cpp util.cpp inductive_cmd.cpp elaborator.cpp
+inductive_cmd.cpp elaborator.cpp dependencies.cpp parser_bindings.cpp
-dependencies.cpp parser_bindings.cpp begin_end_ext.cpp
+begin_end_ext.cpp class.cpp pp_options.cpp tactic_hint.cpp pp.cpp
-class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
+theorem_queue.cpp structure_cmd.cpp info_manager.cpp no_info.cpp
-structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp
+extra_info.cpp local_context.cpp choice_iterator.cpp
-local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp
+placeholder_elaborator.cpp coercion_elaborator.cpp
-coercion_elaborator.cpp proof_qed_elaborator.cpp init_module.cpp)
+proof_qed_elaborator.cpp init_module.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/begin_end_ext.cpp

@@ -27,6 +27,9 @@ struct be_state {
     optional<expr> m_pre_tac_body;
 };
 
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
 struct be_config {
     typedef be_state state;
     typedef be_entry entry;
@@ -44,12 +47,10 @@ struct be_config {
         }
     }
     static name const & get_class_name() {
-        static name g_class_name("begin_end");
+        return *g_class_name;
-        return g_class_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("be_pre_tac");
+        return *g_key;
-        return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
         s << e.m_accumulate << e.m_tac;
@@ -64,6 +65,18 @@ struct be_config {
 template class scoped_ext<be_config>;
 typedef scoped_ext<be_config> begin_end_ext;
 
+void initialize_begin_end_ext() {
+    g_class_name = new name("begin_end");
+    g_key        = new std::string("be_pre_tac");
+    begin_end_ext::initialize();
+}
+
+void finalize_begin_end_ext() {
+    begin_end_ext::finalize();
+    delete g_key;
+    delete g_class_name;
+}
+
 static void check_valid_tactic(environment const & env, expr const & pre_tac) {
     type_checker tc(env);
     if (!tc.is_def_eq(tc.infer(pre_tac).first, get_tactic_type()).first)

src/frontends/lean/begin_end_ext.h

@@ -13,4 +13,7 @@ environment add_begin_end_pre_tactic(environment const & env, expr const & pre_t
 environment reset_begin_end_pre_tactic(environment const & env, expr const & pre_tac);
 optional<expr> get_begin_end_pre_tactic(environment const & env);
 void register_begin_end_cmds(cmd_table & r);
+
+void initialize_begin_end_ext();
+void finalize_begin_end_ext();
 }

src/frontends/lean/calc.cpp

@@ -21,6 +21,7 @@ Author: Leonardo de Moura
 #include "library/scoped_ext.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
+#include "frontends/lean/tokens.h"
 
 namespace lean {
 // Check whether e is of the form (f ...) where f is a constant. If it is return f.
@@ -92,6 +93,9 @@ struct calc_state {
     }
 };
 
+static name * g_calc_name  = nullptr;
+static std::string * g_key = nullptr;
+
 struct calc_config {
     typedef calc_state state;
     typedef calc_entry entry;
@@ -103,12 +107,10 @@ struct calc_config {
         }
     }
     static name const & get_class_name() {
-        static name g_calc_name("calc");
+        return *g_calc_name;
-        return g_calc_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("calc");
+        return *g_key;
-        return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
         s << static_cast<char>(e.m_cmd) << e.m_name;
@@ -153,10 +155,6 @@ inline expr const & pred_lhs(calc_pred const & p) { return std::get<1>(p); }
 inline expr const & pred_rhs(calc_pred const & p) { return std::get<2>(p); }
 inline calc_pred const & step_pred(calc_step const & s) { return s.first; }
 inline expr const & step_proof(calc_step const & s) { return s.second; }
-static name g_lcurly("{");
-static name g_rcurly("}");
-static name g_ellipsis("...");
-static name g_colon(":");
 
 static void decode_expr_core(expr const & e, buffer<calc_pred> & preds) {
     buffer<expr> args;
@@ -196,11 +194,11 @@ static expr mk_op_fn(parser & p, name const & op, unsigned num_placeholders, pos
 static void parse_calc_proof(parser & p, buffer<calc_pred> const & preds, std::vector<calc_step> & steps) {
     steps.clear();
     auto pos = p.pos();
-    p.check_token_next(g_colon, "invalid 'calc' expression, ':' expected");
+    p.check_token_next(get_colon_tk(), "invalid 'calc' expression, ':' expected");
-    if (p.curr_is_token(g_lcurly)) {
+    if (p.curr_is_token(get_lcurly_tk())) {
         p.next();
         expr pr = p.parse_expr();
-        p.check_token_next(g_rcurly, "invalid 'calc' expression, '}' expected");
+        p.check_token_next(get_rcurly_tk(), "invalid 'calc' expression, '}' expected");
         calc_state const & state = calc_ext::get_state(p.env());
         for (auto const & pred : preds) {
             if (auto refl_it = state.m_refl_table.find(pred_op(pred))) {
@@ -265,7 +263,7 @@ expr parse_calc(parser & p) {
     decode_expr(p.parse_expr(), preds, pos);
     parse_calc_proof(p, preds, steps);
     expr dummy     = mk_expr_placeholder();
-    while (p.curr_is_token(g_ellipsis)) {
+    while (p.curr_is_token(get_ellipsis_tk())) {
         pos = p.pos();
         p.next();
         decode_expr(p.parse_led(dummy), preds, pos);
@@ -290,4 +288,16 @@ expr parse_calc(parser & p) {
         choices.push_back(step_proof(s));
     return p.save_pos(mk_choice(choices.size(), choices.data()), pos);
 }
+
+void initialize_calc() {
+    g_calc_name = new name("calc");
+    g_key       = new std::string("calc");
+    calc_ext::initialize();
+}
+
+void finalize_calc() {
+    calc_ext::finalize();
+    delete g_key;
+    delete g_calc_name;
+}
 }

src/frontends/lean/calc.h

@@ -10,4 +10,6 @@ namespace lean {
 class parser;
 void register_calc_cmds(cmd_table & r);
 expr parse_calc(parser & p);
+void initialize_calc();
+void finalize_calc();
 }

src/frontends/lean/class.cpp

@@ -41,6 +41,9 @@ struct class_state {
     }
 };
 
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
 struct class_config {
     typedef class_state state;
     typedef class_entry entry;
@@ -51,12 +54,10 @@ struct class_config {
             s.add_instance(e.m_class, e.m_instance);
     }
     static name const & get_class_name() {
-        static name g_class_name("class");
+        return *g_class_name;
-        return g_class_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("class");
+        return *g_key;
-        return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
         if (e.m_class_cmd)
@@ -78,6 +79,18 @@ struct class_config {
 template class scoped_ext<class_config>;
 typedef scoped_ext<class_config> class_ext;
 
+void initialize_class() {
+    g_class_name = new name("class");
+    g_key = new std::string("class");
+    class_ext::initialize();
+}
+
+void finalize_class() {
+    class_ext::finalize();
+    delete g_key;
+    delete g_class_name;
+}
+
 static void check_class(environment const & env, name const & c_name) {
     declaration c_d = env.get(c_name);
     if (c_d.is_definition() && !c_d.is_opaque())

src/frontends/lean/class.h

@@ -27,4 +27,7 @@ optional<name> is_ext_class(type_checker & tc, expr type);
 
 /** \brief Return a list of instances of the class \c cls_name that occur in \c ctx */
 list<expr> get_local_instances(type_checker & tc, list<expr> const & ctx, name const & cls_name);
+
+void initialize_class();
+void finalize_class();
 }

src/frontends/lean/init_module.cpp

@@ -4,21 +4,39 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "frontends/lean/tokens.h"
 #include "frontends/lean/elaborator.h"
 #include "frontends/lean/pp_options.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/no_info.h"
 #include "frontends/lean/extra_info.h"
+#include "frontends/lean/tactic_hint.h"
+#include "frontends/lean/class.h"
+#include "frontends/lean/parser_config.h"
+#include "frontends/lean/calc.h"
+#include "frontends/lean/begin_end_ext.h"
 
 namespace lean {
 void initialize_frontend_lean_module() {
+    initialize_tokens();
     initialize_elaborator();
     initialize_pp_options();
     initialize_parser();
     initialize_no_info();
     initialize_extra_info();
+    initialize_tactic_hint();
+    initialize_class();
+    initialize_parser_config();
+    initialize_calc();
+    initialize_begin_end_ext();
 }
 void finalize_frontend_lean_module() {
+    finalize_begin_end_ext();
+    finalize_calc();
+    finalize_parser_config();
+    finalize_class();
+    finalize_tactic_hint();
+    finalize_tokens();
     finalize_extra_info();
     finalize_no_info();
     finalize_parser();

src/frontends/lean/parser.cpp

@@ -34,6 +34,7 @@ Author: Leonardo de Moura
 #include "library/sorry.h"
 #include "library/error_handling/error_handling.h"
 #include "library/tactic/expr_to_tactic.h"
+#include "frontends/lean/tokens.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/util.h"
 #include "frontends/lean/parser_bindings.h"
@@ -55,20 +56,6 @@ namespace lean {
 static name * g_parser_show_errors;
 static name * g_parser_parallel_import;
 
-void initialize_parser() {
-    g_parser_show_errors     = new name{"parser", "show_errors"};
-    g_parser_parallel_import = new name{"parser", "parallel_import"};
-    register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
-                         "(lean parser) display error messages in the regular output channel");
-    register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT,
-                         "(lean parser) import modules in parallel");
-}
-
-void finalize_parser() {
-    delete g_parser_show_errors;
-    delete g_parser_parallel_import;
-}
-
 bool get_parser_show_errors(options const & opts) {
     return opts.get_bool(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS);
 }
@@ -94,13 +81,13 @@ parser::no_undef_id_error_scope::~no_undef_id_error_scope() {
     m_p.m_no_undef_id_error = m_old;
 }
 
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
 
 parser::parser(environment const & env, io_state const & ios,
                std::istream & strm, char const * strm_name,
                bool use_exceptions, unsigned num_threads,
                snapshot const * s, snapshot_vector * sv, info_manager * im):
-    m_env(env), m_ios(ios), m_ngen(g_tmp_prefix),
+    m_env(env), m_ios(ios), m_ngen(*g_tmp_prefix),
     m_verbose(true), m_use_exceptions(use_exceptions),
     m_scanner(strm, strm_name, s ? s->m_line : 1),
     m_theorem_queue(*this, num_threads > 1 ? num_threads - 1 : 0),
@@ -455,10 +442,6 @@ unsigned parser::get_local_index(name const & n) const {
     return m_local_decls.find_idx(n);
 }
 
-static name g_period("."), g_colon(":"), g_lparen("("), g_rparen(")"), g_llevel_curly(".{");
-static name g_lcurly("{"), g_rcurly("}"), g_ldcurly("⦃"), g_rdcurly("⦄"), g_lbracket("["), g_rbracket("]");
-static name g_bar("|"), g_comma(","), g_add("+"), g_max("max"), g_imax("imax"), g_cup("\u2294");
-static name g_import("import"), g_show("show"), g_have("have"), g_assume("assume"), g_take("take"), g_fun("fun");
 static unsigned g_level_add_prec = 10;
 static unsigned g_level_cup_prec = 5;
 
@@ -493,9 +476,9 @@ static level lift(level l, unsigned k) {
 }
 
 unsigned parser::curr_level_lbp() const {
-    if (curr_is_token(g_cup))
+    if (curr_is_token(get_cup_tk()))
         return g_level_cup_prec;
-    else if (curr_is_token(g_add))
+    else if (curr_is_token(get_add_tk()))
         return g_level_add_prec;
     else
         return 0;
@@ -505,7 +488,7 @@ level parser::parse_max_imax(bool is_max) {
     auto p = pos();
     next();
     buffer<level> lvls;
-    while (curr_is_identifier() || curr_is_numeral() || curr_is_token(g_lparen)) {
+    while (curr_is_identifier() || curr_is_numeral() || curr_is_token(get_lparen_tk())) {
         lvls.push_back(parse_level());
     }
     if (lvls.size() < 2)
@@ -536,14 +519,14 @@ level parser::parse_level_id() {
 }
 
 level parser::parse_level_nud() {
-    if (curr_is_token_or_id(g_max)) {
+    if (curr_is_token_or_id(get_max_tk())) {
         return parse_max_imax(true);
-    } else if (curr_is_token_or_id(g_imax)) {
+    } else if (curr_is_token_or_id(get_imax_tk())) {
         return parse_max_imax(false);
-    } else if (curr_is_token(g_lparen)) {
+    } else if (curr_is_token(get_lparen_tk())) {
         next();
         level l = parse_level();
-        check_token_next(g_rparen, "invalid level expression, ')' expected");
+        check_token_next(get_rparen_tk(), "invalid level expression, ')' expected");
         return l;
     } else if (curr_is_numeral()) {
         unsigned k = parse_small_nat();
@@ -557,11 +540,11 @@ level parser::parse_level_nud() {
 
 level parser::parse_level_led(level left) {
     auto p = pos();
-    if (curr_is_token(g_cup)) {
+    if (curr_is_token(get_cup_tk())) {
         next();
         level right = parse_level(g_level_cup_prec);
         return mk_max(left, right);
-    } else if (curr_is_token(g_add)) {
+    } else if (curr_is_token(get_add_tk())) {
         next();
         if (curr_is_numeral()) {
             unsigned k = parse_small_nat();
@@ -656,21 +639,21 @@ std::tuple<expr, expr, level_param_names> parser::elaborate_definition_at(enviro
       - '['          : cast
 */
 optional<binder_info> parser::parse_optional_binder_info() {
-    if (curr_is_token(g_lparen)) {
+    if (curr_is_token(get_lparen_tk())) {
         next();
         return some(binder_info());
-    } else if (curr_is_token(g_lcurly)) {
+    } else if (curr_is_token(get_lcurly_tk())) {
         next();
-        if (curr_is_token(g_lcurly)) {
+        if (curr_is_token(get_lcurly_tk())) {
             next();
             return some(mk_strict_implicit_binder_info());
         } else {
             return some(mk_implicit_binder_info());
         }
-    } else if (curr_is_token(g_lbracket)) {
+    } else if (curr_is_token(get_lbracket_tk())) {
         next();
         return some(mk_cast_binder_info());
-    } else if (curr_is_token(g_ldcurly)) {
+    } else if (curr_is_token(get_ldcurly_tk())) {
         next();
         return some(mk_strict_implicit_binder_info());
     } else {
@@ -705,18 +688,18 @@ void parser::parse_close_binder_info(optional<binder_info> const & bi) {
     if (!bi) {
         return;
     } else if (bi->is_implicit()) {
-        check_token_next(g_rcurly, "invalid declaration, '}' expected");
+        check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected");
     } else if (bi->is_cast()) {
-        check_token_next(g_rbracket, "invalid declaration, ']' expected");
+        check_token_next(get_rbracket_tk(), "invalid declaration, ']' expected");
     } else if (bi->is_strict_implicit()) {
-        if (curr_is_token(g_rcurly)) {
+        if (curr_is_token(get_rcurly_tk())) {
             next();
-            check_token_next(g_rcurly, "invalid declaration, '}' expected");
+            check_token_next(get_rcurly_tk(), "invalid declaration, '}' expected");
         } else {
-            check_token_next(g_rdcurly, "invalid declaration, '⦄' expected");
+            check_token_next(get_rdcurly_tk(), "invalid declaration, '⦄' expected");
         }
     } else {
-        check_token_next(g_rparen, "invalid declaration, ')' expected");
+        check_token_next(get_rparen_tk(), "invalid declaration, ')' expected");
     }
 }
 
@@ -725,7 +708,7 @@ expr parser::parse_binder_core(binder_info const & bi) {
     auto p  = pos();
     name id = check_atomic_id_next("invalid binder, atomic identifier expected");
     expr type;
-    if (curr_is_token(g_colon)) {
+    if (curr_is_token(get_colon_tk())) {
         next();
         type = parse_expr();
     } else {
@@ -758,7 +741,7 @@ void parser::parse_binder_block(buffer<expr> & r, binder_info const & bi) {
     if (names.empty())
         throw parser_error("invalid binder, identifier expected", pos());
     optional<expr> type;
-    if (curr_is_token(g_colon)) {
+    if (curr_is_token(get_colon_tk())) {
         next();
         type = parse_expr();
     }
@@ -969,9 +952,9 @@ expr parser::parse_led_notation(expr left) {
 expr parser::id_to_expr(name const & id, pos_info const & p) {
     buffer<level> lvl_buffer;
     levels ls;
-    if (curr_is_token(g_llevel_curly)) {
+    if (curr_is_token(get_llevel_curly_tk())) {
         next();
-        while (!curr_is_token(g_rcurly)) {
+        while (!curr_is_token(get_rcurly_tk())) {
             lvl_buffer.push_back(parse_level());
         }
         next();
@@ -1188,7 +1171,7 @@ static optional<std::string> try_file(std::string const & base, optional<unsigne
     }
 }
 
-static std::string g_lua_module_key("lua_module");
+static std::string * g_lua_module_key = nullptr;
 static void lua_module_reader(deserializer & d, module_idx, shared_environment &,
                               std::function<void(asynch_update_fn const &)> &,
                               std::function<void(delayed_update_fn const &)> & add_delayed_update) {
@@ -1200,20 +1183,19 @@ static void lua_module_reader(deserializer & d, module_idx, shared_environment &
             return env;
         });
 }
-register_module_object_reader_fn g_lua_module_reader(g_lua_module_key, lua_module_reader);
 
 void parser::parse_imports() {
     buffer<module_name> olean_files;
     buffer<name>        lua_files;
     std::string base = dirname(get_stream_name().c_str());
     bool imported    = false;
-    while (curr_is_token(g_import)) {
+    while (curr_is_token(get_import_tk())) {
         imported       = true;
         m_last_cmd_pos = pos();
         next();
         while (true) {
             optional<unsigned> k;
-            while (curr_is_token(g_period)) {
+            while (curr_is_token(get_period_tk())) {
                 next();
                 if (!k)
                     k = 0;
@@ -1250,7 +1232,7 @@ void parser::parse_imports() {
     for (auto const & f : lua_files) {
         std::string rname = find_file(f, {".lua"});
         system_import(rname.c_str());
-        m_env = module::add(m_env, g_lua_module_key, [=](serializer & s) {
+        m_env = module::add(m_env, *g_lua_module_key, [=](serializer & s) {
                 s << f;
             });
     }
@@ -1297,7 +1279,7 @@ bool parser::parse_commands() {
                         done = true;
                         break;
                     case scanner::token_kind::Keyword:
-                        if (curr_is_token(g_period)) {
+                        if (curr_is_token(get_period_tk())) {
                             next();
                             break;
                         }
@@ -1331,7 +1313,7 @@ bool parser::curr_is_command_like() const {
     case scanner::token_kind::Eof:
         return true;
     case scanner::token_kind::Keyword:
-        return curr_is_token(g_period);
+        return curr_is_token(get_period_tk());
     default:
         return false;
     }
@@ -1423,4 +1405,23 @@ bool parse_commands(environment & env, io_state & ios, char const * fname, bool
         throw exception(sstream() << "failed to open file '" << fname << "'");
     return parse_commands(env, ios, in, fname, use_exceptions, num_threads, cache, index);
 }
+
+void initialize_parser() {
+    g_parser_show_errors     = new name{"parser", "show_errors"};
+    g_parser_parallel_import = new name{"parser", "parallel_import"};
+    register_bool_option(*g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS,
+                         "(lean parser) display error messages in the regular output channel");
+    register_bool_option(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT,
+                         "(lean parser) import modules in parallel");
+    g_tmp_prefix = new name(name::mk_internal_unique_name());
+    g_lua_module_key = new std::string("lua_module");
+    register_module_object_reader(*g_lua_module_key, lua_module_reader);
+}
+
+void finalize_parser() {
+    delete g_lua_module_key;
+    delete g_tmp_prefix;
+    delete g_parser_show_errors;
+    delete g_parser_parallel_import;
+}
 }

src/frontends/lean/parser_config.cpp

@@ -33,16 +33,17 @@ struct token_state {
 struct token_config {
     typedef token_state  state;
     typedef token_entry  entry;
+    static name * g_class_name;
+    static std::string * g_key;
+
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
         s.m_table = add_token(s.m_table, e.m_token.c_str(), e.m_prec);
     }
     static name const & get_class_name() {
-        static name g_class_name("notation");
+        return *g_class_name;
-        return g_class_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("tk");
+        return *g_key;
-        return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
         s << e.m_token.c_str() << e.m_prec;
@@ -53,6 +54,8 @@ struct token_config {
         return entry(tk, prec);
     }
 };
+name * token_config::g_class_name = nullptr;
+std::string * token_config::g_key = nullptr;
 
 template class scoped_ext<token_config>;
 typedef scoped_ext<token_config> token_ext;
@@ -154,6 +157,9 @@ struct notation_state {
 struct notation_config {
     typedef notation_state  state;
     typedef notation_entry  entry;
+    static name * g_class_name;
+    static std::string * g_key;
+
     static void add_entry(environment const &, io_state const &, state & s, entry const & e) {
         buffer<transition> ts;
         to_buffer(e.m_transitions, ts);
@@ -163,12 +169,10 @@ struct notation_config {
             s.m_led = s.m_led.add(ts.size(), ts.data(), e.m_expr, e.m_overload);
     }
     static name const & get_class_name() {
-        static name g_class_name("notation");
+        return *g_class_name;
-        return g_class_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("nota");
+        return *g_key;
-        return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
         s << e.m_is_nud << e.m_overload << e.m_expr;
@@ -187,6 +191,8 @@ struct notation_config {
         return entry(is_nud, to_list(ts.begin(), ts.end()), e, overload);
     }
 };
+name * notation_config::g_class_name = nullptr;
+std::string * notation_config::g_key = nullptr;
 
 template class scoped_ext<notation_config>;
 typedef scoped_ext<notation_config> notation_ext;
@@ -251,11 +257,30 @@ struct cmd_ext_reg {
     unsigned m_ext_id;
     cmd_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<cmd_ext>()); }
 };
-static cmd_ext_reg g_ext;
+static cmd_ext_reg * g_ext = nullptr;
 static cmd_ext const & get_extension(environment const & env) {
-    return static_cast<cmd_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<cmd_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 cmd_table const & get_cmd_table(environment const & env) {
     return get_extension(env).m_cmds;
 }
+
+void initialize_parser_config() {
+    token_config::g_class_name = new name("notation");
+    token_config::g_key        = new std::string("tk");
+    token_ext::initialize();
+    notation_config::g_class_name = new name("notation");
+    notation_config::g_key        = new std::string("nota");
+    notation_ext::initialize();
+    g_ext = new cmd_ext_reg();
+}
+void finalize_parser_config() {
+    delete g_ext;
+    notation_ext::finalize();
+    delete notation_config::g_key;
+    delete notation_config::g_class_name;
+    token_ext::finalize();
+    delete token_config::g_key;
+    delete token_config::g_class_name;
+}
 }

src/frontends/lean/parser_config.h

@@ -48,4 +48,7 @@ parse_table const & get_led_table(environment const & env);
 cmd_table const & get_cmd_table(environment const & env);
 /** \brief Force notation from namespace \c n to shadow any existing notation */
 environment overwrite_notation(environment const & env, name const & n);
+
+void initialize_parser_config();
+void finalize_parser_config();
 }

src/frontends/lean/tactic_hint.cpp

@@ -15,6 +15,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/cmd_table.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/class.h"
+#include "frontends/lean/tokens.h"
 
 namespace lean {
 typedef list<tactic_hint_entry> tactic_hint_entries;
@@ -25,6 +26,9 @@ struct tactic_hint_state {
     tactic_hint_entries  m_tactics;
 };
 
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
 struct tactic_hint_config {
     typedef tactic_hint_state   state;
     typedef tactic_hint_entry   entry;
@@ -55,13 +59,11 @@ struct tactic_hint_config {
     }
 
     static name const & get_class_name() {
-        static name g_class_name("tactic_hint");
+        return *g_class_name;
-        return g_class_name;
     }
 
     static std::string const & get_serialization_key() {
-        static std::string g_key("tachint");
+        return *g_key;
-        return g_key;
     }
 
     static void  write_entry(serializer & s, entry const & e) {
@@ -78,6 +80,18 @@ struct tactic_hint_config {
 template class scoped_ext<tactic_hint_config>;
 typedef scoped_ext<tactic_hint_config> tactic_hint_ext;
 
+void initialize_tactic_hint() {
+    g_class_name = new name("tactic_hint");
+    g_key        = new std::string("tachint");
+    tactic_hint_ext::initialize();
+}
+
+void finalize_tactic_hint() {
+    tactic_hint_ext::finalize();
+    delete g_key;
+    delete g_class_name;
+}
+
 list<tactic_hint_entry> get_tactic_hints(environment const & env, name const & c) {
     tactic_hint_state const & s = tactic_hint_ext::get_state(env);
     return ptr_to_list(s.m_class_tactics.find(c));
@@ -101,15 +115,12 @@ expr parse_tactic_name(parser & p) {
     return mk_constant(pre_tac, to_list(ls.begin(), ls.end()));
 }
 
-static name g_lbracket("[");
-static name g_rbracket("]");
-
 environment tactic_hint_cmd(parser & p) {
     name cls;
-    if (p.curr_is_token(g_lbracket)) {
+    if (p.curr_is_token(get_lbracket_tk())) {
         p.next();
         cls      = get_class_name(p.env(), p.parse_expr());
-        p.check_token_next(g_rbracket, "invalid tactic hint, ']' expected");
+        p.check_token_next(get_rbracket_tk(), "invalid tactic hint, ']' expected");
     }
     expr pre_tac = parse_tactic_name(p);
     tactic tac   = expr_to_tactic(p.env(), pre_tac, nullptr);

src/frontends/lean/tactic_hint.h

@@ -27,4 +27,7 @@ list<tactic_hint_entry> get_tactic_hints(environment const & env);
 class parser;
 expr parse_tactic_name(parser & p);
 void register_tactic_hint_cmd(cmd_table & r);
+
+void initialize_tactic_hint();
+void finalize_tactic_hint();
 }

src/frontends/lean/tokens.cpp

@@ -0,0 +1,113 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/name.h"
+
+namespace lean {
+static name * g_period       = nullptr;
+static name * g_colon        = nullptr;
+static name * g_lparen       = nullptr;
+static name * g_rparen       = nullptr;
+static name * g_llevel_curly = nullptr;
+static name * g_lcurly       = nullptr;
+static name * g_rcurly       = nullptr;
+static name * g_ldcurly      = nullptr;
+static name * g_rdcurly      = nullptr;
+static name * g_lbracket     = nullptr;
+static name * g_rbracket     = nullptr;
+static name * g_bar          = nullptr;
+static name * g_comma        = nullptr;
+static name * g_add          = nullptr;
+static name * g_max          = nullptr;
+static name * g_imax         = nullptr;
+static name * g_cup          = nullptr;
+static name * g_import       = nullptr;
+static name * g_show         = nullptr;
+static name * g_have         = nullptr;
+static name * g_assume       = nullptr;
+static name * g_take         = nullptr;
+static name * g_fun          = nullptr;
+static name * g_ellipsis     = nullptr;
+
+void initialize_tokens() {
+    g_period       = new name(".");
+    g_colon        = new name(":");
+    g_lparen       = new name("(");
+    g_rparen       = new name(")");
+    g_llevel_curly = new name(".{");
+    g_lcurly       = new name("{");
+    g_rcurly       = new name("}");
+    g_ldcurly      = new name("⦃");
+    g_rdcurly      = new name("⦄");
+    g_lbracket     = new name("[");
+    g_rbracket     = new name("]");
+    g_bar          = new name("|");
+    g_comma        = new name(",");
+    g_add          = new name("+");
+    g_max          = new name("max");
+    g_imax         = new name("imax");
+    g_cup          = new name("\u2294");
+    g_import       = new name("import");
+    g_show         = new name("show");
+    g_have         = new name("have");
+    g_assume       = new name("assume");
+    g_take         = new name("take");
+    g_fun          = new name("fun");
+    g_ellipsis     = new name("...");
+}
+
+void finalize_tokens() {
+    delete g_ellipsis;
+    delete g_fun;
+    delete g_take;
+    delete g_assume;
+    delete g_have;
+    delete g_show;
+    delete g_import;
+    delete g_cup;
+    delete g_imax;
+    delete g_max;
+    delete g_add;
+    delete g_comma;
+    delete g_bar;
+    delete g_rbracket;
+    delete g_lbracket;
+    delete g_rdcurly;
+    delete g_ldcurly;
+    delete g_lcurly;
+    delete g_rcurly;
+    delete g_llevel_curly;
+    delete g_rparen;
+    delete g_lparen;
+    delete g_colon;
+    delete g_period;
+}
+
+name const & get_period_tk() { return *g_period; }
+name const & get_colon_tk() { return *g_colon; }
+name const & get_lparen_tk() { return *g_lparen; }
+name const & get_rparen_tk() { return *g_rparen; }
+name const & get_llevel_curly_tk() { return *g_llevel_curly; }
+name const & get_lcurly_tk() { return *g_lcurly; }
+name const & get_rcurly_tk() { return *g_rcurly; }
+name const & get_ldcurly_tk() { return *g_ldcurly; }
+name const & get_rdcurly_tk() { return *g_rdcurly; }
+name const & get_lbracket_tk() { return *g_lbracket; }
+name const & get_rbracket_tk() { return *g_rbracket; }
+name const & get_bar_tk() { return *g_bar; }
+name const & get_comma_tk() { return *g_comma; }
+name const & get_add_tk() { return *g_add; }
+name const & get_max_tk() { return *g_max; }
+name const & get_imax_tk() { return *g_imax; }
+name const & get_cup_tk() { return *g_cup; }
+name const & get_import_tk() { return *g_import; }
+name const & get_show_tk() { return *g_show; }
+name const & get_have_tk() { return *g_have; }
+name const & get_assume_tk() { return *g_assume; }
+name const & get_take_tk() { return *g_take; }
+name const & get_fun_tk() { return *g_fun; }
+name const & get_ellipsis_tk() { return *g_ellipsis; }
+}

src/frontends/lean/tokens.h

@@ -0,0 +1,36 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "util/name.h"
+
+namespace lean {
+void initialize_tokens();
+void finalize_tokens();
+name const & get_period_tk();
+name const & get_colon_tk();
+name const & get_lparen_tk();
+name const & get_rparen_tk();
+name const & get_llevel_curly_tk();
+name const & get_lcurly_tk();
+name const & get_rcurly_tk();
+name const & get_ldcurly_tk();
+name const & get_rdcurly_tk();
+name const & get_lbracket_tk();
+name const & get_rbracket_tk();
+name const & get_bar_tk();
+name const & get_comma_tk();
+name const & get_add_tk();
+name const & get_max_tk();
+name const & get_imax_tk();
+name const & get_cup_tk();
+name const & get_import_tk();
+name const & get_show_tk();
+name const & get_have_tk();
+name const & get_assume_tk();
+name const & get_take_tk();
+name const & get_fun_tk();
+name const & get_ellipsis_tk();
+}

src/init/init.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include "util/init_module.h"
 #include "util/sexpr/init_module.h"
 #include "kernel/init_module.h"
+#include "kernel/inductive/inductive.h"
 #include "library/init_module.h"
 #include "library/tactic/init_module.h"
 #include "frontends/lean/init_module.h"
@@ -17,6 +18,7 @@ void initialize() {
     initialize_util_module();
     initialize_sexpr_module();
     initialize_kernel_module();
+    initialize_inductive_module();
     initialize_library_module();
     initialize_tactic_module();
     initialize_frontend_lean_module();
@@ -25,6 +27,7 @@ void finalize() {
     finalize_frontend_lean_module();
     finalize_tactic_module();
     finalize_library_module();
+    finalize_inductive_module();
     finalize_kernel_module();
     finalize_sexpr_module();
     finalize_util_module();

src/kernel/environment.cpp

@@ -169,13 +169,19 @@ public:
     }
 };
 
+static extension_manager * g_extension_manager = nullptr;
 static extension_manager & get_extension_manager() {
-    static std::unique_ptr<extension_manager> g_extension_manager;
-    if (!g_extension_manager)
-        g_extension_manager.reset(new extension_manager());
     return *g_extension_manager;
 }
 
+void initialize_environment() {
+    g_extension_manager = new extension_manager();
+}
+
+void finalize_environment() {
+    delete g_extension_manager;
+}
+
 unsigned environment::register_extension(std::shared_ptr<environment_extension const> const & initial) {
     return get_extension_manager().register_extension(initial);
 }

src/kernel/environment.h

@@ -213,6 +213,10 @@ public:
     void for_each_universe(std::function<void(name const & u)> const & f) const;
 };
 
+void initialize_environment();
+void finalize_environment();
+
+
 class name_generator;
 
 /**

src/kernel/inductive/inductive.cpp

@@ -93,8 +93,8 @@ Author: Leonardo de Moura
 */
 namespace lean {
 namespace inductive {
-static name g_tmp_prefix = name::mk_internal_unique_name();
+static name * g_tmp_prefix = nullptr;
-static name g_inductive_extension("inductive_extension");
+static name * g_inductive_extension = nullptr;
 
 /** \brief Environment extension used to store the computational rules associated with inductive datatype declarations. */
 struct inductive_env_ext : public environment_extension {
@@ -156,16 +156,16 @@ struct inductive_env_ext_reg {
     inductive_env_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<inductive_env_ext>()); }
 };
 
-static inductive_env_ext_reg g_ext;
+static inductive_env_ext_reg * g_ext = nullptr;
 
 /** \brief Retrieve environment extension */
 static inductive_env_ext const & get_extension(environment const & env) {
-    return static_cast<inductive_env_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<inductive_env_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 
 /** \brief Update environment extension */
 static environment update(environment const & env, inductive_env_ext const & ext) {
-    return env.update(g_ext.m_ext_id, std::make_shared<inductive_env_ext>(ext));
+    return env.update(g_ext->m_ext_id, std::make_shared<inductive_env_ext>(ext));
 }
 
 /** \brief Helper functional object for processing inductive datatype declarations. */
@@ -201,7 +201,7 @@ struct add_inductive_fn {
                      unsigned                     num_params,
                      list<inductive_decl> const & decls):
         m_env(env), m_level_names(level_params), m_num_params(num_params), m_decls(decls),
-        m_ngen(g_tmp_prefix), m_tc(new type_checker(m_env)) {
+        m_ngen(*g_tmp_prefix), m_tc(new type_checker(m_env)) {
         m_decls_sz = length(m_decls);
         m_levels = param_names_to_levels(level_params);
     }
@@ -736,7 +736,7 @@ struct add_inductive_fn {
     }
 
     environment operator()() {
-        if (!m_env.norm_ext().supports(g_inductive_extension))
+        if (!m_env.norm_ext().supports(*g_inductive_extension))
             throw kernel_exception(m_env, "environment does not support inductive datatypes");
         if (get_num_its() == 0)
             throw kernel_exception(m_env, "at least one inductive datatype declaration expected");
@@ -758,7 +758,7 @@ environment add_inductive(environment                  env,
 }
 
 bool inductive_normalizer_extension::supports(name const & feature) const {
-    return feature == g_inductive_extension;
+    return feature == *g_inductive_extension;
 }
 
 optional<pair<expr, constraint_seq>> inductive_normalizer_extension::operator()(expr const & e, extension_context & ctx) const {
@@ -879,4 +879,16 @@ optional<unsigned> get_elim_major_idx(environment const & env, name const & n) {
         return optional<unsigned>();
 }
 }
+
+void initialize_inductive_module() {
+    inductive::g_tmp_prefix          = new name(name::mk_internal_unique_name());
+    inductive::g_inductive_extension = new name("inductive_extension");
+    inductive::g_ext                 = new inductive::inductive_env_ext_reg();
+}
+
+void finalize_inductive_module() {
+    delete inductive::g_ext;
+    delete inductive::g_inductive_extension;
+    delete inductive::g_tmp_prefix;
+}
 }

src/kernel/inductive/inductive.h

@@ -68,4 +68,6 @@ optional<name> is_elim_rule(environment const & env, name const & n);
 optional<unsigned> get_elim_major_idx(environment const & env, name const & n);
 bool is_elim_meta_app(type_checker & tc, expr const & e);
 }
+void initialize_inductive_module();
+void finalize_inductive_module();
 }

src/kernel/init_module.cpp

@@ -4,9 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "kernel/environment.h"
 namespace lean {
 void initialize_kernel_module() {
+    initialize_environment();
 }
 void finalize_kernel_module() {
+    finalize_environment();
 }
 }

src/library/aliases.cpp

@@ -119,23 +119,23 @@ struct aliases_ext : public environment_extension {
     }
 };
 
-static name g_aliases("aliases");
+static name * g_aliases = nullptr;
 
 struct aliases_ext_reg {
     unsigned m_ext_id;
     aliases_ext_reg() {
-        register_scoped_ext(g_aliases,
+        register_scoped_ext(*g_aliases,
                             aliases_ext::using_namespace, aliases_ext::export_namespace,
                             aliases_ext::push_scope, aliases_ext::pop_scope);
         m_ext_id = environment::register_extension(std::make_shared<aliases_ext>());
     }
 };
-static aliases_ext_reg g_ext;
+static aliases_ext_reg * g_ext = nullptr;
 static aliases_ext const & get_extension(environment const & env) {
-    return static_cast<aliases_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<aliases_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, aliases_ext const & ext) {
-    return env.update(g_ext.m_ext_id, std::make_shared<aliases_ext>(ext));
+    return env.update(g_ext->m_ext_id, std::make_shared<aliases_ext>(ext));
 }
 
 environment add_expr_alias(environment const & env, name const & a, name const & e) {
@@ -265,4 +265,14 @@ void open_aliases(lua_State * L) {
     SET_GLOBAL_FUN(get_level_alias,  "get_level_alias");
     SET_GLOBAL_FUN(add_aliases,      "add_aliases");
 }
+
+void initialize_aliases() {
+    g_aliases = new name("aliases");
+    g_ext     = new aliases_ext_reg();
+}
+
+void finalize_aliases() {
+    delete g_ext;
+    delete g_aliases;
+}
 }

src/library/aliases.h

@@ -55,4 +55,6 @@ bool is_exception(name const & n, name const & prefix, unsigned num_exceptions,
 void for_each_expr_alias(environment const & env, std::function<void(name const &, list<name> const &)> const & fn);
 
 void open_aliases(lua_State * L);
+void initialize_aliases();
+void finalize_aliases();
 }

src/library/coercion.cpp

@@ -320,6 +320,9 @@ coercion_state add_coercion(environment const & env, io_state const & ios, coerc
     }
 }
 
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
 typedef pair<name, name> coercion_entry;
 struct coercion_config {
     typedef coercion_state  state;
@@ -328,12 +331,10 @@ struct coercion_config {
         s = add_coercion(env, ios, s, e.first, e.second);
     }
     static name const & get_class_name() {
-        static name g_class_name("coercions");
+        return *g_class_name;
-        return g_class_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("coerce");
+        return *g_key;
-        return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
         s << e.first << e.second;
@@ -348,6 +349,18 @@ struct coercion_config {
 template class scoped_ext<coercion_config>;
 typedef scoped_ext<coercion_config> coercion_ext;
 
+void initialize_coercion() {
+    g_class_name = new name("coercions");
+    g_key        = new std::string("coerce");
+    coercion_ext::initialize();
+}
+
+void finalize_coercion() {
+    coercion_ext::finalize();
+    delete g_key;
+    delete g_class_name;
+}
+
 environment add_coercion(environment const & env, name const & f, name const & C, io_state const & ios, bool persistent) {
     return coercion_ext::add_entry(env, ios, coercion_entry(f, C), persistent);
 }

src/library/coercion.h

@@ -97,4 +97,6 @@ void for_each_coercion_user(environment const & env, coercion_user_fn const & f)
 void for_each_coercion_sort(environment const & env, coercion_sort_fn const & f);
 void for_each_coercion_fun(environment const & env, coercion_fun_fn const & f);
 void open_coercion(lua_State * L);
+void initialize_coercion();
+void finalize_coercion();
 }

src/library/init_module.cpp

@@ -13,6 +13,14 @@ Author: Leonardo de Moura
 #include "library/resolve_macro.h"
 #include "library/annotation.h"
 #include "library/explicit.h"
+#include "library/module.h"
+#include "library/protected.h"
+#include "library/private.h"
+#include "library/scoped_ext.h"
+#include "library/reducible.h"
+#include "library/aliases.h"
+#include "library/coercion.h"
+#include "library/unifier_plugin.h"
 
 namespace lean {
 void initialize_library_module() {
@@ -25,9 +33,25 @@ void initialize_library_module() {
     initialize_resolve_macro();
     initialize_annotation();
     initialize_explicit();
+    initialize_module();
+    initialize_protected();
+    initialize_private();
+    initialize_scoped_ext();
+    initialize_reducible();
+    initialize_aliases();
+    initialize_coercion();
+    initialize_unifier_plugin();
 }
 
 void finalize_library_module() {
+    finalize_unifier_plugin();
+    finalize_coercion();
+    finalize_aliases();
+    finalize_reducible();
+    finalize_scoped_ext();
+    finalize_private();
+    finalize_protected();
+    finalize_module();
     finalize_explicit();
     finalize_annotation();
     finalize_resolve_macro();

src/library/module.cpp

@@ -46,12 +46,13 @@ struct module_ext_reg {
     module_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<module_ext>()); }
 };
 
-static module_ext_reg g_ext;
+static module_ext_reg * g_ext = nullptr;
+
 static module_ext const & get_extension(environment const & env) {
-    return static_cast<module_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<module_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, module_ext const & ext) {
-    return env.update(g_ext.m_ext_id, std::make_shared<module_ext>(ext));
+    return env.update(g_ext->m_ext_id, std::make_shared<module_ext>(ext));
 }
 
 static char const * g_olean_end_file = "EndFile";
@@ -113,12 +114,8 @@ void export_module(std::ostream & out, environment const & env) {
 }
 
 typedef std::unordered_map<std::string, module_object_reader> object_readers;
-static std::unique_ptr<object_readers> g_object_readers;
+static object_readers * g_object_readers = nullptr;
-static object_readers & get_object_readers() {
+static object_readers & get_object_readers() { return *g_object_readers; }
-    if (!g_object_readers)
-        g_object_readers.reset(new object_readers());
-    return *(g_object_readers.get());
-}
 
 void register_module_object_reader(std::string const & k, module_object_reader r) {
     object_readers & readers = get_object_readers();
@@ -126,8 +123,9 @@ void register_module_object_reader(std::string const & k, module_object_reader r
     readers[k] = r;
 }
 
-static std::string g_glvl_key("glvl");
+static std::string * g_glvl_key = nullptr;
-static std::string g_decl_key("decl");
+static std::string * g_decl_key = nullptr;
+static std::string * g_inductive = nullptr;
 
 namespace module {
 environment add(environment const & env, std::string const & k, std::function<void(serializer &)> const & wr) {
@@ -138,7 +136,7 @@ environment add(environment const & env, std::string const & k, std::function<vo
 
 environment add_universe(environment const & env, name const & l) {
     environment new_env = env.add_universe(l);
-    return add(new_env, g_glvl_key, [=](serializer & s) { s << l; });
+    return add(new_env, *g_glvl_key, [=](serializer & s) { s << l; });
 }
 
 environment update_module_defs(environment const & env, declaration const & d) {
@@ -155,13 +153,13 @@ environment add(environment const & env, certified_declaration const & d) {
     environment new_env = env.add(d);
     declaration _d = d.get_declaration();
     new_env = update_module_defs(new_env, _d);
-    return add(new_env, g_decl_key, [=](serializer & s) { s << _d; });
+    return add(new_env, *g_decl_key, [=](serializer & s) { s << _d; });
 }
 
 environment add(environment const & env, declaration const & d) {
     environment new_env = env.add(d);
     new_env = update_module_defs(new_env, d);
-    return add(new_env, g_decl_key, [=](serializer & s) { s << d; });
+    return add(new_env, *g_decl_key, [=](serializer & s) { s << d; });
 }
 
 bool is_definition(environment const & env, name const & n) {
@@ -169,14 +167,12 @@ bool is_definition(environment const & env, name const & n) {
     return ext.m_module_defs.contains(n);
 }
 
-static std::string g_inductive("ind");
-
 environment add_inductive(environment                  env,
                           level_param_names const &    level_params,
                           unsigned                     num_params,
                           list<inductive::inductive_decl> const & decls) {
     environment new_env = inductive::add_inductive(env, level_params, num_params, decls);
-    return add(new_env, g_inductive, [=](serializer & s) {
+    return add(new_env, *g_inductive, [=](serializer & s) {
             s << inductive_decls(level_params, num_params, decls);
         });
 }
@@ -194,8 +190,6 @@ environment add_inductive(environment const & env, name const & ind_name, level_
                           unsigned num_params, expr const & type, list<inductive::intro_rule> const & intro_rules) {
     return add_inductive(env, level_params, num_params, to_list(inductive::inductive_decl(ind_name, type, intro_rules)));
 }
-
-static register_module_object_reader_fn g_reg_ind_reader(g_inductive, inductive_reader);
 } // end of namespace module
 
 struct import_modules_fn {
@@ -371,9 +365,9 @@ struct import_modules_fn {
             d >> k;
             if (k == g_olean_end_file) {
                 break;
-            } else if (k == g_decl_key) {
+            } else if (k == *g_decl_key) {
                 import_decl(d, r->m_module_idx);
-            } else if (k == g_glvl_key) {
+            } else if (k == *g_glvl_key) {
                 import_universe(d);
             } else {
                 object_readers & readers = get_object_readers();
@@ -500,4 +494,21 @@ environment import_module(environment const & env, std::string const & base, mod
                           unsigned num_threads, bool keep_proofs, io_state const & ios) {
     return import_modules(env, base, 1, &module, num_threads, keep_proofs, ios);
 }
+
+void initialize_module() {
+    g_ext            = new module_ext_reg();
+    g_object_readers = new object_readers();
+    g_glvl_key       = new std::string("glvl");
+    g_decl_key       = new std::string("decl");
+    g_inductive      = new std::string("ind");
+    register_module_object_reader(*g_inductive, module::inductive_reader);
+}
+
+void finalize_module() {
+    delete g_inductive;
+    delete g_decl_key;
+    delete g_glvl_key;
+    delete g_object_readers;
+    delete g_ext;
+}
 }

src/library/module.h

@@ -71,13 +71,6 @@ typedef void (*module_object_reader)(deserializer & d, module_idx midx, shared_e
 */
 void register_module_object_reader(std::string const & k, module_object_reader r);
 
-/** \brief Auxiliary class for registering module readers when the lean executable is loaded. */
-struct register_module_object_reader_fn {
-    register_module_object_reader_fn(std::string const & k, module_object_reader r) {
-        register_module_object_reader(k, r);
-    }
-};
-
 namespace module {
 /** \brief Add a function that should be invoked when the environment is exported.
     The key \c k identifies which module_object_reader should be used to deserialize the object
@@ -118,4 +111,7 @@ environment add_inductive(environment const &        env,
                           list<inductive::intro_rule> const & intro_rules);     // introduction rules
 
 }
+
+void initialize_module();
+void finalize_module();
 }

src/library/private.cpp

@@ -23,21 +23,21 @@ struct private_ext_reg {
     private_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<private_ext>()); }
 };
 
-static private_ext_reg g_ext;
+static private_ext_reg * g_ext = nullptr;
 static private_ext const & get_extension(environment const & env) {
-    return static_cast<private_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<private_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, private_ext const & ext) {
-    return env.update(g_ext.m_ext_id, std::make_shared<private_ext>(ext));
+    return env.update(g_ext->m_ext_id, std::make_shared<private_ext>(ext));
 }
 
-static name g_private("private");
+static name * g_private = nullptr;
-static std::string g_prv_key("prv");
+static std::string * g_prv_key = nullptr;
 
 // Make sure the mapping "hidden-name r ==> user-name n" is preserved when we close sections and
 // export .olean files.
 static environment preserve_private_data(environment const & env, name const & r, name const & n) {
-    return module::add(env, g_prv_key, [=](serializer & s) { s << n << r; });
+    return module::add(env, *g_prv_key, [=](serializer & s) { s << n << r; });
 }
 
 pair<environment, name> add_private_name(environment const & env, name const & n, optional<unsigned> const & extra_hash) {
@@ -45,7 +45,7 @@ pair<environment, name> add_private_name(environment const & env, name const & n
     unsigned h      = hash(n.hash(), ext.m_counter);
     if (extra_hash)
         h = hash(h, *extra_hash);
-    name r = name(g_private, h) + n;
+    name r = name(*g_private, h) + n;
     ext.m_inv_map.insert(r, n);
     ext.m_counter++;
     environment new_env = update(env, ext);
@@ -67,8 +67,6 @@ static void private_reader(deserializer & d, module_idx, shared_environment & se
         });
 }
 
-register_module_object_reader_fn g_private_reader(g_prv_key, private_reader);
-
 optional<name> hidden_to_user_name(environment const & env, name const & n) {
     auto it = get_extension(env).m_inv_map.find(n);
     return it ? optional<name>(*it) : optional<name>();
@@ -85,10 +83,25 @@ static int add_private_name(lua_State * L) {
     return 2;
 }
 
-static int hidden_to_user_name(lua_State * L) { return push_optional_name(L, hidden_to_user_name(to_environment(L, 1), to_name_ext(L, 2))); }
+static int hidden_to_user_name(lua_State * L) {
+    return push_optional_name(L, hidden_to_user_name(to_environment(L, 1), to_name_ext(L, 2)));
+}
 
 void open_private(lua_State * L) {
     SET_GLOBAL_FUN(add_private_name,    "add_private_name");
     SET_GLOBAL_FUN(hidden_to_user_name, "hidden_to_user_name");
 }
+
+void initialize_private() {
+    g_ext     = new private_ext_reg();
+    g_private = new name("private");
+    g_prv_key = new std::string("prv");
+    register_module_object_reader(*g_prv_key, private_reader);
+}
+
+void finalize_private() {
+    delete g_prv_key;
+    delete g_private;
+    delete g_ext;
+}
 }

src/library/private.h

@@ -32,4 +32,6 @@ pair<environment, name> add_private_name(environment const & env, name const & n
 optional<name> hidden_to_user_name(environment const & env, name const & n);
 
 void open_private(lua_State * L);
+void initialize_private();
+void finalize_private();
 }

src/library/protected.cpp

@@ -20,21 +20,21 @@ struct protected_ext_reg {
     protected_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<protected_ext>()); }
 };
 
-static protected_ext_reg g_ext;
+static protected_ext_reg * g_ext = nullptr;
 static protected_ext const & get_extension(environment const & env) {
-    return static_cast<protected_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<protected_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, protected_ext const & ext) {
-    return env.update(g_ext.m_ext_id, std::make_shared<protected_ext>(ext));
+    return env.update(g_ext->m_ext_id, std::make_shared<protected_ext>(ext));
 }
 
-static std::string g_prt_key("prt");
+static std::string * g_prt_key = nullptr;
 
 environment add_protected(environment const & env, name const & n) {
     protected_ext ext = get_extension(env);
     ext.m_protected.insert(n);
     environment new_env = update(env, ext);
-    return module::add(new_env, g_prt_key, [=](serializer & s) { s << n; });
+    return module::add(new_env, *g_prt_key, [=](serializer & s) { s << n; });
 }
 
 static void protected_reader(deserializer & d, module_idx, shared_environment & senv,
@@ -49,9 +49,18 @@ static void protected_reader(deserializer & d, module_idx, shared_environment &
         });
 }
 
-register_module_object_reader_fn g_protected_reader(g_prt_key, protected_reader);
-
 bool is_protected(environment const & env, name const & n) {
     return get_extension(env).m_protected.contains(n);
 }
+
+void initialize_protected() {
+    g_ext     = new protected_ext_reg();
+    g_prt_key = new std::string("prt");
+    register_module_object_reader(*g_prt_key, protected_reader);
+}
+
+void finalize_protected() {
+    delete g_prt_key;
+    delete g_ext;
+}
 }

src/library/protected.h

@@ -12,4 +12,7 @@ namespace lean {
 environment add_protected(environment const & env, name const & n);
 /** \brief Return true iff \c n was marked as protected in the environment \c n. */
 bool is_protected(environment const & env, name const & n);
+
+void initialize_protected();
+void finalize_protected();
 }

src/library/reducible.cpp

@@ -13,7 +13,6 @@ Author: Leonardo de Moura
 #include "library/reducible.h"
 
 namespace lean {
-
 struct reducible_entry {
     reducible_status m_status;
     name             m_name;
@@ -43,6 +42,9 @@ struct reducible_state {
     }
 };
 
+static name * g_class_name = nullptr;
+static std::string * g_key = nullptr;
+
 struct reducible_config {
     typedef reducible_state  state;
     typedef reducible_entry  entry;
@@ -50,12 +52,10 @@ struct reducible_config {
         s.add(e);
     }
     static name const & get_class_name() {
-        static name g_class_name("reducible");
+         return *g_class_name;
-        return g_class_name;
     }
     static std::string const & get_serialization_key() {
-        static std::string g_key("redu");
+        return *g_key;
-        return g_key;
     }
     static void  write_entry(serializer & s, entry const & e) {
         s << static_cast<char>(e.m_status) << e.m_name;
@@ -71,6 +71,18 @@ struct reducible_config {
 template class scoped_ext<reducible_config>;
 typedef scoped_ext<reducible_config> reducible_ext;
 
+void initialize_reducible() {
+    g_class_name = new name("reducible");
+    g_key        = new std::string("redu");
+    reducible_ext::initialize();
+}
+
+void finalize_reducible() {
+    reducible_ext::finalize();
+    delete g_key;
+    delete g_class_name;
+}
+
 static void check_declaration(environment const & env, name const & n) {
     declaration const & d = env.get(n);
     if (!d.is_definition())

src/library/reducible.h

@@ -36,4 +36,7 @@ bool is_reducible_off(environment const & env, name const & n);
 /** \brief Create a type checker that takes the "reducibility" hints into account. */
 std::unique_ptr<type_checker> mk_type_checker(environment const & env, name_generator const & ngen,
                                               bool relax_main_opaque, bool only_main_reducible = false);
+
+void initialize_reducible();
+void finalize_reducible();
 }

src/library/scoped_ext.cpp

@@ -14,13 +14,8 @@ Author: Leonardo de Moura
 namespace lean {
 typedef std::tuple<name, using_namespace_fn, export_namespace_fn, push_scope_fn, pop_scope_fn> entry;
 typedef std::vector<entry> scoped_exts;
-
+static scoped_exts * g_exts = nullptr;
-static scoped_exts & get_exts() {
+static scoped_exts & get_exts() { return *g_exts; }
-    static std::unique_ptr<std::vector<entry>> exts;
-    if (!exts.get())
-        exts.reset(new std::vector<entry>());
-    return *exts;
-}
 
 void register_scoped_ext(name const & c, using_namespace_fn use, export_namespace_fn ex, push_scope_fn push, pop_scope_fn pop) {
     get_exts().emplace_back(c, use, ex, push, pop);
@@ -38,12 +33,12 @@ struct scope_mng_ext_reg {
     scope_mng_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<scope_mng_ext>()); }
 };
 
-static scope_mng_ext_reg g_ext;
+static scope_mng_ext_reg * g_ext = nullptr;
 static scope_mng_ext const & get_extension(environment const & env) {
-    return static_cast<scope_mng_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<scope_mng_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, scope_mng_ext const & ext) {
-    return env.update(g_ext.m_ext_id, std::make_shared<scope_mng_ext>(ext));
+    return env.update(g_ext->m_ext_id, std::make_shared<scope_mng_ext>(ext));
 }
 
 name const & get_namespace(environment const & env) {
@@ -95,7 +90,7 @@ optional<name> to_valid_namespace_name(environment const & env, name const & n)
     return optional<name>();
 }
 
-static std::string g_new_namespace_key("nspace");
+static std::string * g_new_namespace_key = nullptr;
 environment push_scope(environment const & env, io_state const & ios, scope_kind k, name const & n) {
     if (k == scope_kind::Namespace && in_section_or_context(env))
         throw exception("invalid namespace declaration, a namespace cannot be declared inside a section or context");
@@ -118,7 +113,7 @@ environment push_scope(environment const & env, io_state const & ios, scope_kind
     if (k == scope_kind::Namespace)
         r = using_namespace(r, ios, n);
     if (save_ns)
-        r = module::add(r, g_new_namespace_key, [=](serializer & s) { s << new_n; });
+        r = module::add(r, *g_new_namespace_key, [=](serializer & s) { s << new_n; });
     return r;
 }
 
@@ -133,14 +128,14 @@ static void namespace_reader(deserializer & d, module_idx, shared_environment &,
             return update(env, ext);
         });
 }
-register_module_object_reader_fn g_namespace_reader(g_new_namespace_key, namespace_reader);
 
 environment pop_scope(environment const & env, name const & n) {
     scope_mng_ext ext = get_extension(env);
     if (is_nil(ext.m_namespaces))
         throw exception("invalid end of scope, there are no open namespaces/sections/contexts");
     if (n != head(ext.m_headers))
-        throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '" << head(ext.m_headers) << "', and ends with '" << n << "'");
+        throw exception(sstream() << "invalid end of scope, begin/end mistmatch, scope starts with '"
+                        << head(ext.m_headers) << "', and ends with '" << n << "'");
     scope_kind k      = head(ext.m_scope_kinds);
     ext.m_namespaces  = tail(ext.m_namespaces);
     ext.m_headers     = tail(ext.m_headers);
@@ -201,4 +196,17 @@ void open_scoped_ext(lua_State * L) {
     SET_ENUM("Context",     scope_kind::Context);
     lua_setglobal(L, "scope_kind");
 }
+
+void initialize_scoped_ext() {
+    g_exts = new scoped_exts();
+    g_ext  = new scope_mng_ext_reg();
+    g_new_namespace_key = new std::string("nspace");
+    register_module_object_reader(*g_new_namespace_key, namespace_reader);
+}
+
+void finalize_scoped_ext() {
+    delete g_new_namespace_key;
+    delete g_exts;
+    delete g_ext;
+}
 }

src/library/scoped_ext.h

@@ -161,12 +161,15 @@ public:
         }
     };
 
-    static reg g_ext;
+    static reg * g_ext;
+    static void initialize() { g_ext = new reg(); }
+    static void finalize() { delete g_ext; }
+
     static scoped_ext const & get(environment const & env) {
-        return static_cast<scoped_ext const &>(env.get_extension(g_ext.m_ext_id));
+        return static_cast<scoped_ext const &>(env.get_extension(g_ext->m_ext_id));
     }
     static environment update(environment const & env, scoped_ext const & ext) {
-        return env.update(g_ext.m_ext_id, std::make_shared<scoped_ext>(ext));
+        return env.update(g_ext->m_ext_id, std::make_shared<scoped_ext>(ext));
     }
     static environment using_namespace_fn(environment const & env, io_state const & ios, name const & n) {
         return update(env, get(env).using_namespace(env, ios, n));
@@ -222,5 +225,8 @@ public:
 };
 
 template<typename Config, bool TransientSection>
-typename scoped_ext<Config, TransientSection>::reg scoped_ext<Config, TransientSection>::g_ext;
+typename scoped_ext<Config, TransientSection>::reg * scoped_ext<Config, TransientSection>::g_ext = nullptr;
+
+void initialize_scoped_ext();
+void finalize_scoped_ext();
 }

src/library/unifier_plugin.cpp

@@ -66,12 +66,20 @@ struct unifier_plugin_ext_reg {
     unifier_plugin_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<unifier_plugin_ext>()); }
 };
 
-static unifier_plugin_ext_reg g_ext;
+static unifier_plugin_ext_reg * g_ext = nullptr;
 static unifier_plugin_ext const & get_extension(environment const & env) {
-    return static_cast<unifier_plugin_ext const &>(env.get_extension(g_ext.m_ext_id));
+    return static_cast<unifier_plugin_ext const &>(env.get_extension(g_ext->m_ext_id));
 }
 static environment update(environment const & env, unifier_plugin_ext const & ext) {
-    return env.update(g_ext.m_ext_id, std::make_shared<unifier_plugin_ext>(ext));
+    return env.update(g_ext->m_ext_id, std::make_shared<unifier_plugin_ext>(ext));
+}
+
+void initialize_unifier_plugin() {
+    g_ext = new unifier_plugin_ext_reg();
+}
+
+void finalize_unifier_plugin() {
+    delete g_ext;
 }
 
 environment set_unifier_plugin(environment const & env, unifier_plugin const & p) {

src/library/unifier_plugin.h

@@ -35,4 +35,6 @@ unifier_plugin orelse(unifier_plugin const & p1, unifier_plugin const & p2);
 
 environment set_unifier_plugin(environment const & env, unifier_plugin const & p);
 unifier_plugin const & get_unifier_plugin(environment const & env);
+void initialize_unifier_plugin();
+void finalize_unifier_plugin();
 }

src/tests/frontends/lean/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_executable(lean_scanner scanner.cpp)
-target_link_libraries(lean_scanner "lean_frontend" "library" "kernel" "util" ${EXTRA_LIBS})
+target_link_libraries(lean_scanner "init" "lean_frontend" "library" "kernel" "util" ${EXTRA_LIBS})
 add_test(lean_scanner ${CMAKE_CURRENT_BINARY_DIR}/lean_scanner)
 # add_executable(lean_parser parser.cpp)
 # target_link_libraries(lean_parser ${ALL_LIBS})

src/tests/frontends/lean/scanner.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/exception.h"
 #include "frontends/lean/scanner.h"
 #include "frontends/lean/parser_config.h"
+#include "init/init.h"
 using namespace lean;
 
 #define tk scanner::token_kind
@@ -197,9 +198,11 @@ static void tst4(unsigned N) {
 
 int main() {
     save_stack_info();
+    initialize();
     tst1();
     tst2();
     tst3();
     tst4(100000);
+    finalize();
     return has_violations() ? 1 : 0;
 }

src/tests/kernel/environment.cpp

@@ -8,10 +8,14 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/exception.h"
 #include "util/trace.h"
+#include "util/init_module.h"
+#include "util/sexpr/init_module.h"
 #include "kernel/environment.h"
 #include "kernel/type_checker.h"
 #include "kernel/abstract.h"
 #include "kernel/kernel_exception.h"
+#include "kernel/init_module.h"
+#include "library/init_module.h"
 #include "library/print.h"
 using namespace lean;
 
@@ -241,6 +245,10 @@ public:
 
 int main() {
     save_stack_info();
+    initialize_util_module();
+    initialize_sexpr_module();
+    initialize_kernel_module();
+    initialize_library_module();
     init_default_print_fn();
     tst1();
     tst2();
@@ -248,5 +256,9 @@ int main() {
     tst4();
     environment_id_tester::tst1();
     environment_id_tester::tst2();
+    finalize_library_module();
+    finalize_kernel_module();
+    finalize_sexpr_module();
+    finalize_util_module();
     return has_violations() ? 1 : 0;
 }

src/tests/library/unifier.cpp

@@ -5,6 +5,10 @@ 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/init_module.h"
+#include "library/init_module.h"
 #include "library/unifier.h"
 using namespace lean;
 
@@ -24,6 +28,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;
 }