refactor(*): start move to explicit initialization/finalization,

explicitly initialize/finalize options

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

src/CMakeLists.txt

@@ -262,6 +262,8 @@ add_subdirectory(frontends/lean)
 set(LEAN_LIBS ${LEAN_LIBS} lean_frontend)
 add_subdirectory(frontends/lua)
 set(LEAN_LIBS ${LEAN_LIBS} leanlua)
+add_subdirectory(init)
+set(LEAN_LIBS ${LEAN_LIBS} init)
 set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} ${LEAN_EXTRA_LINKER_FLAGS}")
 if(("${MULTI_THREAD}" MATCHES "ON") AND (NOT (("${CMAKE_SYSTEM_NAME}" MATCHES "Darwin") AND ("${BOOST}" MATCHES "ON"))))
    set(CMAKE_EXE_LINKER_FLAGS "${CMAKE_EXE_LINKER_FLAGS} -pthread")

src/frontends/lean/CMakeLists.txt

@@ -7,6 +7,6 @@ dependencies.cpp parser_bindings.cpp begin_end_ext.cpp
 class.cpp pp_options.cpp tactic_hint.cpp pp.cpp theorem_queue.cpp
 structure_cmd.cpp info_manager.cpp no_info.cpp extra_info.cpp
 local_context.cpp choice_iterator.cpp placeholder_elaborator.cpp
-coercion_elaborator.cpp proof_qed_elaborator.cpp)
+coercion_elaborator.cpp proof_qed_elaborator.cpp init_module.cpp)
 
 target_link_libraries(lean_frontend ${LEAN_LIBS})

src/frontends/lean/elaborator.cpp

@@ -11,6 +11,7 @@ Author: Leonardo de Moura
 #include "util/lazy_list_fn.h"
 #include "util/sstream.h"
 #include "util/name_map.h"
+#include "util/sexpr/option_declarations.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
@@ -54,10 +55,21 @@ Author: Leonardo de Moura
 namespace lean {
 // ==========================================
 // elaborator configuration options
-static name g_elaborator_local_instances{"elaborator", "local_instances"};
-RegisterBoolOption(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES, "(lean elaborator) use local declarates as class instances");
+static name * g_elaborator_local_instances = nullptr;
+
+void initialize_elaborator() {
+    g_elaborator_local_instances = new name{"elaborator", "local_instances"};
+
+    register_bool_option(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES,
+                         "(lean elaborator) use local declarates as class instances");
+}
+
+void finalize_elaborator() {
+    delete g_elaborator_local_instances;
+}
+
 bool get_elaborator_local_instances(options const & opts) {
-    return opts.get_bool(g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES);
+    return opts.get_bool(*g_elaborator_local_instances, LEAN_DEFAULT_ELABORATOR_LOCAL_INSTANCES);
 }
 // ==========================================
 

src/frontends/lean/elaborator.h

@@ -36,4 +36,6 @@ std::tuple<expr, level_param_names> elaborate(elaborator_context & env, list<exp
 
 std::tuple<expr, expr, level_param_names> elaborate(elaborator_context & env, name const & n, expr const & t, expr const & v,
                                                     bool is_opaque);
+void initialize_elaborator();
+void finalize_elaborator();
 }

src/frontends/lean/init_module.cpp

@@ -0,0 +1,22 @@
+/*
+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 "frontends/lean/elaborator.h"
+#include "frontends/lean/pp_options.h"
+#include "frontends/lean/parser.h"
+
+namespace lean {
+void initialize_frontend_lean_module() {
+    initialize_elaborator();
+    initialize_pp_options();
+    initialize_parser();
+}
+void finalize_frontend_lean_module() {
+    finalize_parser();
+    finalize_pp_options();
+    finalize_elaborator();
+}
+}

src/frontends/lean/init_module.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+void initialize_frontend_lean_module();
+void finalize_frontend_lean_module();
+}

src/frontends/lean/parser.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/flet.h"
 #include "util/lean_path.h"
+#include "util/sexpr/option_declarations.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/replace_fn.h"
 #include "kernel/abstract.h"
@@ -51,14 +52,30 @@ Author: Leonardo de Moura
 namespace lean {
 // ==========================================
 // Parser configuration options
-static name g_parser_show_errors     {"parser", "show_errors"};
-static name g_parser_parallel_import {"parser", "parallel_import"};
+static name * g_parser_show_errors;
+static name * g_parser_parallel_import;
 
-RegisterBoolOption(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS, "(lean parser) display error messages in the regular output channel");
-RegisterBoolOption(g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT, "(lean parser) import modules in parallel");
+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");
+}
 
-bool     get_parser_show_errors(options const & opts)  { return opts.get_bool(g_parser_show_errors, LEAN_DEFAULT_PARSER_SHOW_ERRORS); }
-bool     get_parser_parallel_import(options const & opts)  { return opts.get_bool(g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT); }
+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);
+}
+
+bool get_parser_parallel_import(options const & opts) {
+    return opts.get_bool(*g_parser_parallel_import, LEAN_DEFAULT_PARSER_PARALLEL_IMPORT);
+}
 // ==========================================
 
 parser::local_scope::local_scope(parser & p):

src/frontends/lean/parser.h

@@ -355,4 +355,7 @@ bool parse_commands(environment & env, io_state & ios, std::istream & in, char c
                     declaration_index * index = nullptr);
 bool parse_commands(environment & env, io_state & ios, char const * fname, bool use_exceptions, unsigned num_threads,
                     definition_cache * cache = nullptr, declaration_index * index = nullptr);
+
+void initialize_parser();
+void finalize_parser();
 }

src/frontends/lean/pp_options.cpp

@@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 
 Author: Leonardo de Moura
 */
+#include "util/sexpr/option_declarations.h"
 #include "frontends/lean/pp_options.h"
 
 #ifndef LEAN_DEFAULT_PP_MAX_DEPTH
@@ -47,61 +48,87 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-static name g_pp_max_depth        {"pp", "max_depth"};
-static name g_pp_max_steps        {"pp", "max_steps"};
-static name g_pp_notation         {"pp", "notation"};
-static name g_pp_implicit         {"pp", "implicit"};
-static name g_pp_coercions        {"pp", "coercions"};
-static name g_pp_universes        {"pp", "universes"};
-static name g_pp_full_names       {"pp", "full_names"};
-static name g_pp_private_names    {"pp", "private_names"};
-static name g_pp_metavar_args     {"pp", "metavar_args"};
-static name g_pp_beta             {"pp", "beta"};
+static name * g_pp_max_depth     = nullptr;
+static name * g_pp_max_steps     = nullptr;
+static name * g_pp_notation      = nullptr;
+static name * g_pp_implicit      = nullptr;
+static name * g_pp_coercions     = nullptr;
+static name * g_pp_universes     = nullptr;
+static name * g_pp_full_names    = nullptr;
+static name * g_pp_private_names = nullptr;
+static name * g_pp_metavar_args  = nullptr;
+static name * g_pp_beta          = nullptr;
+static list<options> * g_distinguishing_pp_options = nullptr;
 
-name const & get_pp_coercions_option_name() { return g_pp_coercions; }
-name const & get_pp_full_names_option_name() { return g_pp_full_names; }
+void initialize_pp_options() {
+    g_pp_max_depth     = new name{"pp", "max_depth"};
+    g_pp_max_steps     = new name{"pp", "max_steps"};
+    g_pp_notation      = new name{"pp", "notation"};
+    g_pp_implicit      = new name{"pp", "implicit"};
+    g_pp_coercions     = new name{"pp", "coercions"};
+    g_pp_universes     = new name{"pp", "universes"};
+    g_pp_full_names    = new name{"pp", "full_names"};
+    g_pp_private_names = new name{"pp", "private_names"};
+    g_pp_metavar_args  = new name{"pp", "metavar_args"};
+    g_pp_beta          = new name{"pp", "beta"};
+    register_unsigned_option(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
+                             "(pretty printer) maximum expression depth, after that it will use ellipsis");
+    register_unsigned_option(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS,
+                             "(pretty printer) maximum number of visited expressions, after that it will use ellipsis");
+    register_bool_option(*g_pp_notation,  LEAN_DEFAULT_PP_NOTATION,
+                         "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)");
+    register_bool_option(*g_pp_implicit,  LEAN_DEFAULT_PP_IMPLICIT,
+                         "(pretty printer) display implicit parameters");
+    register_bool_option(*g_pp_coercions,  LEAN_DEFAULT_PP_COERCIONS,
+                         "(pretty printer) display coercionss");
+    register_bool_option(*g_pp_universes,  LEAN_DEFAULT_PP_UNIVERSES,
+                         "(pretty printer) display universes");
+    register_bool_option(*g_pp_full_names,  LEAN_DEFAULT_PP_FULL_NAMES,
+                         "(pretty printer) display fully qualified names");
+    register_bool_option(*g_pp_private_names,  LEAN_DEFAULT_PP_PRIVATE_NAMES,
+                         "(pretty printer) display internal names assigned to private declarations");
+    register_bool_option(*g_pp_metavar_args,  LEAN_DEFAULT_PP_METAVAR_ARGS,
+                         "(pretty printer) display metavariable arguments");
+    register_bool_option(*g_pp_beta,  LEAN_DEFAULT_PP_BETA,
+                         "(pretty printer) apply beta-reduction when pretty printing");
 
-list<options> const & get_distinguishing_pp_options() {
-    static options g_universes_true(g_pp_universes, true);
-    static options g_implicit_true(g_pp_implicit, true);
-    static options g_coercions_true(g_pp_coercions, true);
-    static options g_notation_false(g_pp_notation, false);
-    static options g_implicit_coercions = join(g_coercions_true, g_implicit_true);
-    static options g_implicit_notation = join(g_notation_false, g_implicit_true);
-    static options g_all = join(join(g_universes_true, g_implicit_true), join(g_coercions_true, g_notation_false));
-    static list<options> g_distinguishing_pp_options({g_implicit_true, g_coercions_true, g_implicit_coercions, g_implicit_notation, g_universes_true, g_all});
-    return g_distinguishing_pp_options;
+    options universes_true(*g_pp_universes, true);
+    options implicit_true(*g_pp_implicit, true);
+    options coercions_true(*g_pp_coercions, true);
+    options notation_false(*g_pp_notation, false);
+    options implicit_coercions = join(coercions_true, implicit_true);
+    options implicit_notation  = join(notation_false, implicit_true);
+    options all = join(join(universes_true, implicit_true), join(coercions_true, notation_false));
+    g_distinguishing_pp_options = new list<options>({implicit_true, coercions_true, implicit_coercions,
+                implicit_notation, universes_true, all});
 }
 
-RegisterUnsignedOption(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH,
-                       "(pretty printer) maximum expression depth, after that it will use ellipsis");
-RegisterUnsignedOption(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS,
-                       "(pretty printer) maximum number of visited expressions, after that it will use ellipsis");
-RegisterBoolOption(g_pp_notation,  LEAN_DEFAULT_PP_NOTATION,
-                   "(pretty printer) disable/enable notation (infix, mixfix, postfix operators and unicode characters)");
-RegisterBoolOption(g_pp_implicit,  LEAN_DEFAULT_PP_IMPLICIT,
-                   "(pretty printer) display implicit parameters");
-RegisterBoolOption(g_pp_coercions,  LEAN_DEFAULT_PP_COERCIONS,
-                   "(pretty printer) display coercionss");
-RegisterBoolOption(g_pp_universes,  LEAN_DEFAULT_PP_UNIVERSES,
-                   "(pretty printer) display universes");
-RegisterBoolOption(g_pp_full_names,  LEAN_DEFAULT_PP_FULL_NAMES,
-                   "(pretty printer) display fully qualified names");
-RegisterBoolOption(g_pp_private_names,  LEAN_DEFAULT_PP_PRIVATE_NAMES,
-                   "(pretty printer) display internal names assigned to private declarations");
-RegisterBoolOption(g_pp_metavar_args,  LEAN_DEFAULT_PP_METAVAR_ARGS,
-                   "(pretty printer) display metavariable arguments");
-RegisterBoolOption(g_pp_beta,  LEAN_DEFAULT_PP_BETA,
-                   "(pretty printer) apply beta-reduction when pretty printing");
-
-unsigned get_pp_max_depth(options const & opts)     { return opts.get_unsigned(g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
-unsigned get_pp_max_steps(options const & opts)     { return opts.get_unsigned(g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
-bool     get_pp_notation(options const & opts)      { return opts.get_bool(g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
-bool     get_pp_implicit(options const & opts)      { return opts.get_bool(g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
-bool     get_pp_coercions(options const & opts)     { return opts.get_bool(g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); }
-bool     get_pp_universes(options const & opts)     { return opts.get_bool(g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
-bool     get_pp_full_names(options const & opts)    { return opts.get_bool(g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
-bool     get_pp_private_names(options const & opts) { return opts.get_bool(g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }
-bool     get_pp_metavar_args(options const & opts)  { return opts.get_bool(g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); }
-bool     get_pp_beta(options const & opts)          { return opts.get_bool(g_pp_beta, LEAN_DEFAULT_PP_BETA); }
+void finalize_pp_options() {
+    delete g_pp_max_depth;
+    delete g_pp_max_steps;
+    delete g_pp_notation;
+    delete g_pp_implicit;
+    delete g_pp_coercions;
+    delete g_pp_universes;
+    delete g_pp_full_names;
+    delete g_pp_private_names;
+    delete g_pp_metavar_args;
+    delete g_pp_beta;
+    delete g_distinguishing_pp_options;
+}
+
+name const & get_pp_coercions_option_name() { return *g_pp_coercions; }
+name const & get_pp_full_names_option_name() { return *g_pp_full_names; }
+
+unsigned get_pp_max_depth(options const & opts)     { return opts.get_unsigned(*g_pp_max_depth, LEAN_DEFAULT_PP_MAX_DEPTH); }
+unsigned get_pp_max_steps(options const & opts)     { return opts.get_unsigned(*g_pp_max_steps, LEAN_DEFAULT_PP_MAX_STEPS); }
+bool     get_pp_notation(options const & opts)      { return opts.get_bool(*g_pp_notation, LEAN_DEFAULT_PP_NOTATION); }
+bool     get_pp_implicit(options const & opts)      { return opts.get_bool(*g_pp_implicit, LEAN_DEFAULT_PP_IMPLICIT); }
+bool     get_pp_coercions(options const & opts)     { return opts.get_bool(*g_pp_coercions, LEAN_DEFAULT_PP_COERCIONS); }
+bool     get_pp_universes(options const & opts)     { return opts.get_bool(*g_pp_universes, LEAN_DEFAULT_PP_UNIVERSES); }
+bool     get_pp_full_names(options const & opts)    { return opts.get_bool(*g_pp_full_names, LEAN_DEFAULT_PP_FULL_NAMES); }
+bool     get_pp_private_names(options const & opts) { return opts.get_bool(*g_pp_private_names, LEAN_DEFAULT_PP_PRIVATE_NAMES); }
+bool     get_pp_metavar_args(options const & opts)  { return opts.get_bool(*g_pp_metavar_args, LEAN_DEFAULT_PP_METAVAR_ARGS); }
+bool     get_pp_beta(options const & opts)          { return opts.get_bool(*g_pp_beta, LEAN_DEFAULT_PP_BETA); }
+list<options> const & get_distinguishing_pp_options() { return *g_distinguishing_pp_options; }
 }

src/frontends/lean/pp_options.h

@@ -21,4 +21,7 @@ bool     get_pp_private_names(options const & opts);
 bool     get_pp_metavar_args(options const & opts);
 bool     get_pp_beta(options const & opts);
 list<options> const & get_distinguishing_pp_options();
+
+void initialize_pp_options();
+void finalize_pp_options();
 }

src/init/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_library(init init.cpp)
+
+target_link_libraries(init ${LEAN_LIBS})

src/init/init.cpp

@@ -0,0 +1,34 @@
+/*
+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/sexpr/init_module.h"
+#include "library/init_module.h"
+#include "library/tactic/init_module.h"
+#include "frontends/lean/init_module.h"
+#include "init/init.h"
+
+namespace lean {
+void initialize() {
+    initialize_sexpr_module();
+    initialize_library_module();
+    initialize_tactic_module();
+    initialize_frontend_lean_module();
+}
+void finalize() {
+    finalize_frontend_lean_module();
+    finalize_tactic_module();
+    finalize_library_module();
+    finalize_sexpr_module();
+}
+
+initializer::initializer() {
+    initialize();
+}
+
+initializer::~initializer() {
+    finalize();
+}
+}

src/init/init.h

@@ -0,0 +1,18 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+void initialize();
+void finalize();
+/** \brief Helper object for initializing Lean */
+class initializer {
+public:
+    initializer();
+    ~initializer();
+};
+}

src/library/CMakeLists.txt

@@ -9,6 +9,6 @@ add_library(library deep_copy.cpp expr_lt.cpp io_state.cpp occurs.cpp
   explicit.cpp num.cpp string.cpp head_map.cpp match.cpp
   definition_cache.cpp declaration_index.cpp
   print.cpp annotation.cpp typed_expr.cpp let.cpp type_util.cpp
-  protected.cpp metavar_closure.cpp reducible.cpp)
+  protected.cpp metavar_closure.cpp reducible.cpp init_module.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/init_module.cpp

@@ -0,0 +1,17 @@
+/*
+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 "library/unifier.h"
+
+namespace lean {
+void initialize_library_module() {
+    initialize_unifier();
+}
+
+void finalize_library_module() {
+    finalize_unifier();
+}
+}

src/library/init_module.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+void initialize_library_module();
+void finalize_library_module();
+}

src/library/tactic/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(tactic goal.cpp proof_state.cpp tactic.cpp apply_tactic.cpp
-expr_to_tactic.cpp)
+expr_to_tactic.cpp init_module.cpp)
 
 # simplify_tactic.cpp)
 

src/library/tactic/init_module.cpp

@@ -0,0 +1,17 @@
+/*
+Copyright (c) 2013-2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "library/tactic/proof_state.h"
+
+namespace lean {
+void initialize_tactic_module() {
+    initialize_proof_state();
+}
+
+void finalize_tactic_module() {
+    finalize_proof_state();
+}
+}

src/library/tactic/init_module.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+void initialize_tactic_module();
+void finalize_tactic_module();
+}

src/library/tactic/proof_state.cpp

@@ -7,6 +7,7 @@ Author: Leonardo de Moura
 #include <utility>
 #include "util/sstream.h"
 #include "util/interrupt.h"
+#include "util/sexpr/option_declarations.h"
 #include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
 #include "kernel/abstract.h"
@@ -23,9 +24,21 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-static name g_proof_state_goal_names          {"tactic", "goal_names"};
-RegisterBoolOption(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES, "(tactic) display goal names when pretty printing proof state");
-bool get_proof_state_goal_names(options const & opts) { return opts.get_bool(g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES); }
+static name * g_proof_state_goal_names = nullptr;
+
+void initialize_proof_state() {
+    g_proof_state_goal_names = new name{"tactic", "goal_names"};
+    register_bool_option(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES,
+                         "(tactic) display goal names when pretty printing proof state");
+}
+
+void finalize_proof_state() {
+    delete g_proof_state_goal_names;
+}
+
+bool get_proof_state_goal_names(options const & opts) {
+    return opts.get_bool(*g_proof_state_goal_names, LEAN_PROOF_STATE_GOAL_NAMES);
+}
 
 format proof_state::pp(formatter const & fmt) const {
     options const & opts = fmt.get_options();

src/library/tactic/proof_state.h

@@ -46,4 +46,7 @@ io_state_stream const & operator<<(io_state_stream const & out, proof_state cons
 UDATA_DEFS_CORE(goals)
 UDATA_DEFS(proof_state)
 void open_proof_state(lua_State * L);
+
+void initialize_proof_state();
+void finalize_proof_state();
 }

src/library/unifier.cpp

@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "util/sstream.h"
 #include "util/lbool.h"
 #include "util/flet.h"
+#include "util/sexpr/option_declarations.h"
 #include "kernel/for_each_fn.h"
 #include "kernel/abstract.h"
 #include "kernel/instantiate.h"
@@ -42,20 +43,38 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-static name g_unifier_max_steps      {"unifier", "max_steps"};
-RegisterUnsignedOption(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps");
-unsigned get_unifier_max_steps(options const & opts) { return opts.get_unsigned(g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS); }
+static name * g_unifier_max_steps         = nullptr;
+static name * g_unifier_computation       = nullptr;
+static name * g_unifier_expensive_classes = nullptr;
 
-static name g_unifier_computation    {"unifier", "computation"};
-RegisterBoolOption(g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION,
-                   "(unifier) always case-split on reduction/computational steps when solving flex-rigid and delta-delta constraints");
-bool get_unifier_computation(options const & opts) { return opts.get_bool(g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION); }
+void initialize_unifier() {
+    g_unifier_max_steps         = new name{"unifier", "max_steps"};
+    g_unifier_computation       = new name{"unifier", "computation"};
+    g_unifier_expensive_classes = new name{"unifier", "expensive_classes"};
+
+    register_unsigned_option(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS, "(unifier) maximum number of steps");
+    register_bool_option(*g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION,
+                         "(unifier) always case-split on reduction/computational steps when solving flex-rigid and delta-delta constraints");
+    register_bool_option(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES,
+                         "(unifier) use \"full\" higher-order unification when solving class instances");
+}
+
+void finalize_unifier() {
+    delete g_unifier_max_steps;
+    delete g_unifier_computation;
+    delete g_unifier_expensive_classes;
+}
+
+unsigned get_unifier_max_steps(options const & opts) {
+    return opts.get_unsigned(*g_unifier_max_steps, LEAN_DEFAULT_UNIFIER_MAX_STEPS);
+}
+
+bool get_unifier_computation(options const & opts) {
+    return opts.get_bool(*g_unifier_computation, LEAN_DEFAULT_UNIFIER_COMPUTATION);
+}
 
-static name g_unifier_expensive_classes {"unifier", "expensive_classes"};
-RegisterBoolOption(g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES,
-                   "(unifier) use \"full\" higher-order unification when solving class instances");
 bool get_unifier_expensive_classes(options const & opts) {
-    return opts.get_bool(g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES);
+    return opts.get_bool(*g_unifier_expensive_classes, LEAN_DEFAULT_UNIFIER_EXPENSIVE_CLASSES);
 }
 
 unifier_config::unifier_config(bool use_exceptions, bool discard):

src/library/unifier.h

@@ -95,4 +95,7 @@ public:
 };
 
 void open_unifier(lua_State * L);
+
+void initialize_unifier();
+void finalize_unifier();
 }

src/shell/lean.cpp

@@ -35,6 +35,7 @@ Author: Leonardo de Moura
 #include "frontends/lean/server.h"
 #include "frontends/lean/dependencies.h"
 #include "frontends/lua/register_modules.h"
+#include "init/init.h"
 #include "version.h"
 #include "githash.h" // NOLINT
 
@@ -197,6 +198,7 @@ int main(int argc, char ** argv) {
     lean::save_stack_info();
     lean::init_default_print_fn();
     lean::register_modules();
+    lean::initializer init;
     bool export_objects  = false;
     unsigned trust_lvl   = 0;
     bool server          = false;

src/tests/util/format.cpp

@@ -14,6 +14,7 @@ Author: Soonho Kong
 #include "util/sexpr/format.h"
 #include "util/sexpr/sexpr_fn.h"
 #include "util/sexpr/options.h"
+#include "util/sexpr/init_module.h"
 using namespace lean;
 
 using std::cout;
@@ -126,11 +127,13 @@ static void tst6() {
 
 int main() {
     save_stack_info();
+    initialize_sexpr_module();
     tst1();
     tst2();
     tst3();
     tst4();
     tst5();
     tst6();
+    finalize_sexpr_module();
     return has_violations() ? 1 : 0;
 }

src/tests/util/options.cpp

@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/test.h"
 #include "util/sexpr/options.h"
 #include "util/sexpr/option_declarations.h"
+#include "util/sexpr/init_module.h"
 using namespace lean;
 
 static void tst1() {
@@ -128,8 +129,6 @@ static void tst4() {
     lean_assert(s.str() == "Bool Int Unsigned Int Double String S-Expression");
 }
 
-RegisterBoolOption("fakeopt", false, "fake option");
-
 static void tst5() {
     option_declarations const & decls = get_option_declarations();
     auto it = decls.find("fakeopt");
@@ -156,11 +155,17 @@ static void tst6() {
 
 int main() {
     save_stack_info();
+    initialize_sexpr_module();
+    name fakeopt("fakeopt");
+    register_bool_option(fakeopt, false, "fake option");
+
     tst1();
     tst2();
     tst3();
     tst4();
     tst5();
     tst6();
+
+    finalize_sexpr_module();
     return has_violations() ? 1 : 0;
 }

src/tests/util/sexpr.cpp

@@ -13,6 +13,7 @@ Author: Leonardo de Moura
 #include "util/sexpr/sexpr_fn.h"
 #include "util/sexpr/format.h"
 #include "util/sexpr/options.h"
+#include "util/sexpr/init_module.h"
 using namespace lean;
 
 static void tst1() {
@@ -239,6 +240,7 @@ static void tst10() {
 
 int main() {
     save_stack_info();
+    initialize_sexpr_module();
     tst1();
     tst2();
     tst3();
@@ -249,5 +251,6 @@ int main() {
     tst8();
     tst9();
     tst10();
+    finalize_sexpr_module();
     return has_violations() ? 1 : 0;
 }

src/util/sexpr/CMakeLists.txt

@@ -1,2 +1,4 @@
-add_library(sexpr sexpr.cpp sexpr_fn.cpp format.cpp options.cpp option_declarations.cpp)
+add_library(sexpr sexpr.cpp sexpr_fn.cpp format.cpp options.cpp
+  option_declarations.cpp init_module.cpp)
+
 target_link_libraries(sexpr ${LEAN_LIBS})

src/util/sexpr/format.cpp

@@ -18,6 +18,7 @@
 #include "util/sexpr/format.h"
 #include "util/sexpr/sexpr_fn.h"
 #include "util/sexpr/options.h"
+#include "util/sexpr/option_declarations.h"
 
 #ifndef LEAN_DEFAULT_PP_INDENTATION
 #define LEAN_DEFAULT_PP_INDENTATION 2
@@ -48,32 +49,41 @@
 #endif
 
 namespace lean {
-static name g_pp_indent{"pp", "indent"};
-static name g_pp_unicode{"pp", "unicode"};
-static name g_pp_colors{"pp", "colors"};
-static name g_pp_width{"pp", "width"};
+static name * g_pp_indent  = nullptr;
+static name * g_pp_unicode = nullptr;
+static name * g_pp_colors  = nullptr;
+static name * g_pp_width   = nullptr;
 
-RegisterUnsignedOption(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION, "(pretty printer) default indentation");
-RegisterBoolOption(g_pp_unicode, LEAN_DEFAULT_PP_UNICODE, "(pretty printer) use unicode characters");
-RegisterBoolOption(g_pp_colors, LEAN_DEFAULT_PP_COLORS, "(pretty printer) use colors");
-RegisterUnsignedOption(g_pp_width, LEAN_DEFAULT_PP_WIDTH, "(pretty printer) line width");
+void initialize_format() {
+    g_pp_indent  = new name{"pp", "indent"};
+    g_pp_unicode = new name{"pp", "unicode"};
+    g_pp_colors  = new name{"pp", "colors"};
+    g_pp_width   = new name{"pp", "width"};
+    register_unsigned_option(*g_pp_indent, LEAN_DEFAULT_PP_INDENTATION, "(pretty printer) default indentation");
+    register_bool_option(*g_pp_unicode, LEAN_DEFAULT_PP_UNICODE, "(pretty printer) use unicode characters");
+    register_bool_option(*g_pp_colors, LEAN_DEFAULT_PP_COLORS, "(pretty printer) use colors");
+    register_unsigned_option(*g_pp_width, LEAN_DEFAULT_PP_WIDTH, "(pretty printer) line width");
+}
+
+void finalize_format() {
+    delete g_pp_indent;
+    delete g_pp_unicode;
+    delete g_pp_colors;
+    delete g_pp_width;
+}
 
 unsigned get_pp_indent(options const & o) {
-    return o.get_unsigned(g_pp_indent, LEAN_DEFAULT_PP_INDENTATION);
+    return o.get_unsigned(*g_pp_indent, LEAN_DEFAULT_PP_INDENTATION);
 }
-
 bool get_pp_unicode(options const & o) {
-    return o.get_bool(g_pp_unicode, LEAN_DEFAULT_PP_UNICODE);
+    return o.get_bool(*g_pp_unicode, LEAN_DEFAULT_PP_UNICODE);
 }
-
 bool get_pp_colors(options const & o) {
-    return o.get_bool(g_pp_colors, LEAN_DEFAULT_PP_COLORS);
+    return o.get_bool(*g_pp_colors, LEAN_DEFAULT_PP_COLORS);
 }
-
 unsigned get_pp_width(options const & o) {
-    return o.get_unsigned(g_pp_width, LEAN_DEFAULT_PP_WIDTH);
+    return o.get_unsigned(*g_pp_width, LEAN_DEFAULT_PP_WIDTH);
 }
-
 format compose(format const & f1, format const & f2) {
     return format(format::sexpr_compose({f1.m_value, f2.m_value}));
 }

src/util/sexpr/format.h

@@ -323,4 +323,7 @@ bool format_pp_eq(format const & f1, format const & f2, options const & o);
 
 UDATA_DEFS(format)
 void open_format(lua_State * L);
+
+void initialize_format();
+void finalize_format();
 }

src/util/sexpr/init_module.cpp

@@ -0,0 +1,23 @@
+/*
+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/sexpr/option_declarations.h"
+#include "util/sexpr/options.h"
+#include "util/sexpr/format.h"
+
+namespace lean {
+void initialize_sexpr_module() {
+    initialize_option_declarations();
+    initialize_options();
+    initialize_format();
+}
+
+void finalize_sexpr_module() {
+    finalize_format();
+    finalize_options();
+    finalize_option_declarations();
+}
+}

src/util/sexpr/init_module.h

@@ -0,0 +1,12 @@
+/*
+Copyright (c) 2014 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#pragma once
+
+namespace lean {
+void initialize_sexpr_module();
+void finalize_sexpr_module();
+}

src/util/sexpr/option_declarations.cpp

@@ -51,4 +51,22 @@ void option_declaration::display_value(std::ostream & out, options const & o) co
     if (!contains)
         out << get_default_value();
 }
+
+static option_declarations * g_option_declarations = nullptr;
+
+void initialize_option_declarations() {
+    g_option_declarations = new option_declarations();
+}
+
+void finalize_option_declarations() {
+    delete g_option_declarations;
+}
+
+option_declarations const & get_option_declarations() {
+    return *g_option_declarations;
+}
+
+void register_option(name const & n, option_kind k, char const * default_value, char const * description) {
+    g_option_declarations->insert(mk_pair(n, option_declaration(n, k, default_value, description)));
+}
 }

src/util/sexpr/option_declarations.h

@@ -32,5 +32,10 @@ public:
 };
 
 typedef std::map<name, option_declaration> option_declarations;
+void initialize_option_declarations();
+void finalize_option_declarations();
 option_declarations const & get_option_declarations();
+void register_option(name const & n, option_kind k, char const * default_value, char const * description);
+#define register_bool_option(n, v, d) register_option(n, BoolOption, #v, d)
+#define register_unsigned_option(n, v, d) register_option(n, UnsignedOption, #v, d)
 }

src/util/sexpr/options.cpp

@@ -16,9 +16,20 @@ Author: Leonardo de Moura
 #endif
 
 namespace lean {
-static name g_verbose("verbose");
-RegisterBoolOption(g_verbose,  LEAN_DEFAULT_VERBOSE, "disable/enable verbose messages");
-bool get_verbose(options const & opts) { return opts.get_bool(g_verbose, LEAN_DEFAULT_VERBOSE); }
+static name * g_verbose = nullptr;
+
+void initialize_options() {
+    g_verbose = new name("verbose");
+    register_bool_option(*g_verbose, LEAN_DEFAULT_VERBOSE, "disable/enable verbose messages");
+}
+
+void finalize_options() {
+    delete g_verbose;
+}
+
+bool get_verbose(options const & opts) {
+    return opts.get_bool(*g_verbose, LEAN_DEFAULT_VERBOSE);
+}
 
 std::ostream & operator<<(std::ostream & out, option_kind k) {
     switch (k) {
@@ -32,19 +43,6 @@ std::ostream & operator<<(std::ostream & out, option_kind k) {
     return out;
 }
 
-option_declarations & get_option_declarations_core() {
-    static option_declarations g_option_declarations;
-    return g_option_declarations;
-}
-
-option_declarations const & get_option_declarations() {
-    return get_option_declarations_core();
-}
-
-mk_option_declaration::mk_option_declaration(name const & n, option_kind k, char const * default_value, char const * description) {
-    get_option_declarations_core().insert(mk_pair(n, option_declaration(n, k, default_value, description)));
-}
-
 bool options::empty() const {
     return is_nil(m_value);
 }

src/util/sexpr/options.h

@@ -114,4 +114,7 @@ options get_global_options(lua_State * L);
 */
 void set_global_options(lua_State * L, options const & o);
 void open_options(lua_State * L);
+
+void initialize_options();
+void finalize_options();
 }