chore(library/init/lean): export as C functions

library/init/lean/elaborator/basic.lean

@@ -334,7 +334,7 @@ partial def processCommandsAux : Unit → Frontend Unit
 def processCommands : Frontend Unit :=
 processCommandsAux ()
 
-@[export lean.absolutize_module_name_core]
+@[export lean_absolutize_module_name]
 def absolutizeModuleName (baseDir : Option String) (m : Name) (k : Option Nat) : IO Name :=
 match k, baseDir with
 | none,   _            => pure m

library/init/lean/elaborator/elabstrategyattrs.lean

@@ -27,7 +27,7 @@ registerEnumAttributes `elaboratorStrategy
 @[init mkElaboratorStrategyAttrs]
 constant elaboratorStrategyAttrs : EnumAttributes ElaboratorStrategy := default _
 
-@[export lean.get_elaborator_strategy_core]
+@[export lean_get_elaborator_strategy]
 def getElaboratorStrategy (env : Environment) (n : Name) : Option ElaboratorStrategy :=
 elaboratorStrategyAttrs.getValue env n
 

library/init/lean/eqncompiler/matchpattern.lean

@@ -15,7 +15,7 @@ registerTagAttribute `matchPattern "mark that a definition can be used in a patt
 @[init mkMatchPatternAttr]
 constant matchPatternAttr : TagAttribute := default _
 
-@[export lean.has_match_pattern_attribute_core]
+@[export lean_has_match_pattern_attribute]
 def hasMatchPatternAttribute (env : Environment) (n : Name) : Bool :=
 matchPatternAttr.hasTag env n
 

library/init/lean/parser/module.lean

@@ -97,7 +97,7 @@ private partial def testModuleParserAux (env : Environment) (c : ParserContextCo
       when displayStx (IO.println stx);
       testModuleParserAux s messages
 
-@[export lean.test_module_parser_core]
+@[export lean_test_module_parser]
 def testModuleParser (env : Environment) (input : String) (fileName := "<input>") (displayStx := false) : IO Bool :=
 timeit (fileName ++ " parser") $ do
   let ctx                := mkParserContextCore env input fileName;

library/init/lean/path.lean

@@ -55,7 +55,7 @@ do val ← IO.getEnv "LEAN_PATH";
    | none     => pure ["."] -- If LEAN_PATH is not defined, use current directory
    | some val => pure (val.split searchPathSep)
 
-@[export lean.init_search_path_core]
+@[export lean_init_search_path]
 def initSearchPath (path : Option String := "") : IO Unit :=
 match path with
 | some path => setSearchPathFromString path
@@ -97,7 +97,7 @@ realPathNormalized fname
 def findOLean (modName : Name) : IO String :=
 findLeanFile modName "olean"
 
-@[export lean.find_lean_core]
+@[export lean_find_lean]
 def findLean (modName : Name) : IO String :=
 findLeanFile modName "lean"
 
@@ -108,7 +108,7 @@ do fname ← realPathNormalized fname;
    | some r => pure r
    | none   => throw (IO.userError ("file '" ++ fname ++ "' not in the search path " ++ repr paths))
 
-@[export lean.module_name_of_file_core]
+@[export lean_module_name_of_file]
 def moduleNameOfFileName (fname : String) : IO Name :=
 do
 path  ← findAtSearchPath fname;

library/init/lean/projfns.lean

@@ -30,13 +30,13 @@ registerSimplePersistentEnvExtension {
 @[init mkProjectionFnInfoExtension]
 constant projectionFnInfoExt : SimplePersistentEnvExtension (Name × ProjectionFunctionInfo) (NameMap ProjectionFunctionInfo) := default _
 
-@[export lean.add_projection_info_core]
+@[export lean_add_projection_info]
 def addProjectionFnInfo (env : Environment) (projName : Name) (ctorName : Name) (nparams : Nat) (i : Nat) (fromClass : Bool) : Environment :=
 projectionFnInfoExt.addEntry env (projName, { ctorName := ctorName, nparams := nparams, i := i, fromClass := fromClass })
 
 namespace Environment
 
-@[export lean.get_projection_info_core]
+@[export lean_get_projection_info]
 def getProjectionFnInfo (env : Environment) (projName : Name) : Option ProjectionFunctionInfo :=
 match env.getModuleIdxFor projName with
 | some modIdx =>

library/init/system/io.lean

@@ -41,7 +41,7 @@ instance : Inhabited IO.Error := inferInstanceAs (Inhabited String)
 def IO.userError (s : String) : IO.Error :=
 s
 
-@[export lean.io_error_to_string_core]
+@[export lean_io_error_to_string]
 def IO.Error.toString : IO.Error → String :=
 id
 

src/frontends/lean/elaborator.cpp

@@ -65,10 +65,10 @@ bool get_elaborator_coercions(options const & opts) {
     return opts.get_bool(*g_elaborator_coercions, LEAN_DEFAULT_ELABORATOR_COERCIONS);
 }
 
-object* get_elaborator_strategy_core(object* env, object *n);
+extern "C" object* lean_get_elaborator_strategy(object* env, object *n);
 
 elaborator_strategy get_elaborator_strategy(environment const & env, name const & n) {
-    optional<elaborator_strategy> st = to_optional_scalar<elaborator_strategy>(get_elaborator_strategy_core(env.to_obj_arg(), n.to_obj_arg()));
+    optional<elaborator_strategy> st = to_optional_scalar<elaborator_strategy>(lean_get_elaborator_strategy(env.to_obj_arg(), n.to_obj_arg()));
     if (st)
         return *st;
 

src/library/pattern_attribute.cpp

@@ -7,9 +7,9 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 
 namespace lean {
-uint8 has_match_pattern_attribute_core(object*, object*);
+extern "C" uint8 lean_has_match_pattern_attribute(object*, object*);
 
 bool has_pattern_attribute(environment const & env, name const & d) {
-    return has_match_pattern_attribute_core(env.to_obj_arg(), d.to_obj_arg());
+    return lean_has_match_pattern_attribute(env.to_obj_arg(), d.to_obj_arg());
 }
 }

src/library/projection.cpp

@@ -18,15 +18,15 @@ projection_info::projection_info(name const & c, unsigned nparams, unsigned i, b
     cnstr_set_scalar<unsigned char>(raw(), 3*sizeof(object*), static_cast<unsigned char>(inst_implicit));
 }
 
-object* add_projection_info_core(object* env, object* p, object* ctor, object* nparams, object* i, uint8 fromClass);
-object* get_projection_info_core(object* env, object* p);
+extern "C" object* lean_add_projection_info(object* env, object* p, object* ctor, object* nparams, object* i, uint8 fromClass);
+extern "C" object* lean_get_projection_info(object* env, object* p);
 
 environment save_projection_info(environment const & env, name const & p, name const & mk, unsigned nparams, unsigned i, bool inst_implicit) {
-    return environment(add_projection_info_core(env.to_obj_arg(), p.to_obj_arg(), mk.to_obj_arg(), mk_nat_obj(nparams), mk_nat_obj(i), inst_implicit));
+    return environment(lean_add_projection_info(env.to_obj_arg(), p.to_obj_arg(), mk.to_obj_arg(), mk_nat_obj(nparams), mk_nat_obj(i), inst_implicit));
 }
 
 optional<projection_info> get_projection_info(environment const & env, name const & p) {
-    return to_optional<projection_info>(get_projection_info_core(env.to_obj_arg(), p.to_obj_arg()));
+    return to_optional<projection_info>(lean_get_projection_info(env.to_obj_arg(), p.to_obj_arg()));
 }
 
 /** \brief Return true iff the type named \c S can be viewed as

src/shell/lean.cpp

@@ -296,28 +296,28 @@ public:
 };
 
 namespace lean {
-object* test_module_parser_core(object* env, object* input, object* filename, uint8 displayCtx, object* w);
+extern "C" object* lean_test_module_parser(object* env, object* input, object* filename, uint8 displayCtx, object* w);
 bool test_module_parser(environment const & env, std::string const & input, std::string const & filename) {
-    return get_io_scalar_result<bool>(test_module_parser_core(env.to_obj_arg(), mk_string(input), mk_string(filename), false, io_mk_world()));
+    return get_io_scalar_result<bool>(lean_test_module_parser(env.to_obj_arg(), mk_string(input), mk_string(filename), false, io_mk_world()));
 }
 
-object* init_search_path_core(object* opt_path, object* w);
+extern "C" object* lean_init_search_path(object* opt_path, object* w);
 
 void init_search_path() {
-    get_io_scalar_result<unsigned>(init_search_path_core(mk_option_none(), io_mk_world()));
+    get_io_scalar_result<unsigned>(lean_init_search_path(mk_option_none(), io_mk_world()));
 }
 
-object* find_lean_core(object* mod_name, object* w);
+extern "C" object* lean_find_lean(object* mod_name, object* w);
 
 std::string find_lean_file(name mod_name) {
-    string_ref fname = get_io_result<string_ref>(find_lean_core(mod_name.to_obj_arg(), io_mk_world()));
+    string_ref fname = get_io_result<string_ref>(lean_find_lean(mod_name.to_obj_arg(), io_mk_world()));
     return fname.to_std_string();
 }
 
-object* module_name_of_file_core(object* fname, object* w);
+extern "C" object* lean_module_name_of_file(object* fname, object* w);
 
 name module_name_of_file2(std::string const & fname) {
-    return get_io_result<name>(module_name_of_file_core(mk_string(fname), io_mk_world()));
+    return get_io_result<name>(lean_module_name_of_file(mk_string(fname), io_mk_world()));
 }
 }
 

src/stage0/init/lean/elaborator/basic.cpp

@@ -86,9 +86,7 @@ obj* l_Lean_Elab_getElabContext___boxed(obj*, obj*);
 obj* l_Lean_SMap_find___at_Lean_Elab_elabCommand___spec__1(obj*, obj*);
 obj* l_Lean_Elab_logError___rarg(obj*, obj*, obj*, obj*);
 extern "C" obj* lean_import_modules(obj*, uint32, obj*);
-namespace lean {
-obj* absolutize_module_name_core(obj*, obj*, obj*, obj*);
-}
+extern "C" obj* lean_absolutize_module_name(obj*, obj*, obj*, obj*);
 obj* l_Lean_Elab_logError(obj*);
 obj* l_List_reverse___rarg(obj*);
 obj* l_Lean_Elab_processCommandsAux___main(obj*);
@@ -188,9 +186,7 @@ uint8 nat_dec_lt(obj*, obj*);
 obj* l_Lean_Elab_runElab___rarg___boxed(obj*, obj*, obj*);
 obj* l_RBNode_find___main___at_Lean_addBuiltinCommandElab___spec__4___boxed(obj*, obj*);
 obj* l_Lean_Elab_resolveNamespaceUsingScopes___boxed(obj*, obj*, obj*);
-namespace lean {
-obj* module_name_of_file_core(obj*, obj*);
-}
+extern "C" obj* lean_module_name_of_file(obj*, obj*);
 extern obj* l_Lean_PersistentEnvExtension_inhabited___rarg___closed__1;
 obj* l_Lean_Syntax_getArgs___rarg(obj*);
 obj* l_Lean_Elab_processHeaderAux___boxed(obj*, obj*, obj*, obj*);
@@ -16712,8 +16708,7 @@ x_1 = lean::mk_string("invalid use of relative import, file name of main file is
 return x_1;
 }
 }
-namespace lean {
-obj* absolutize_module_name_core(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
+obj* lean_absolutize_module_name(obj* x_1, obj* x_2, obj* x_3, obj* x_4) {
 _start:
 {
 if (lean::obj_tag(x_3) == 0)
@@ -16794,13 +16789,12 @@ x_22 = l_Array_mfindAux___main___at_Lean_findFile___spec__2___closed__1;
 x_23 = lean::string_append(x_21, x_22);
 x_24 = l_Lean_findOLean___closed__1;
 x_25 = lean::string_append(x_23, x_24);
-x_26 = lean::module_name_of_file_core(x_25, x_4);
+x_26 = lean_module_name_of_file(x_25, x_4);
 return x_26;
 }
 }
 }
 }
-}
 obj* l_Array_miterateAux___main___at_Lean_Elab_processHeaderAux___spec__1(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
 _start:
 {
@@ -16866,7 +16860,7 @@ lean::dec(x_18);
 x_26 = l_Lean_Syntax_getId___rarg(x_25);
 lean::dec(x_25);
 lean::inc(x_1);
-x_27 = lean::absolutize_module_name_core(x_1, x_26, x_24, x_7);
+x_27 = lean_absolutize_module_name(x_1, x_26, x_24, x_7);
 if (lean::obj_tag(x_27) == 0)
 {
 uint8 x_28; 
@@ -16944,7 +16938,7 @@ lean::dec(x_18);
 x_45 = l_Lean_Syntax_getId___rarg(x_44);
 lean::dec(x_44);
 lean::inc(x_1);
-x_46 = lean::absolutize_module_name_core(x_1, x_45, x_43, x_7);
+x_46 = lean_absolutize_module_name(x_1, x_45, x_43, x_7);
 if (lean::obj_tag(x_46) == 0)
 {
 uint8 x_47; 

src/stage0/init/lean/elaborator/elabstrategyattrs.cpp

@@ -101,9 +101,7 @@ obj* l_Lean_PersistentEnvExtension_addEntry___rarg(obj*, obj*, obj*);
 obj* l_IO_Prim_Ref_get(obj*, obj*, obj*);
 uint8 l_Lean_Name_quickLt(obj*, obj*);
 obj* l_Lean_mkElaboratorStrategyAttrs___closed__1;
-namespace lean {
-obj* get_elaborator_strategy_core(obj*, obj*);
-}
+extern "C" obj* lean_get_elaborator_strategy(obj*, obj*);
 obj* l_Array_size(obj*, obj*);
 obj* l_Lean_elaboratorStrategyAttrs;
 obj* l_Array_binSearchAux___main___at_Lean_getElaboratorStrategy___spec__3___boxed(obj*, obj*, obj*, obj*);
@@ -3160,8 +3158,7 @@ return x_25;
 }
 }
 }
-namespace lean {
-obj* get_elaborator_strategy_core(obj* x_1, obj* x_2) {
+obj* lean_get_elaborator_strategy(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; obj* x_4; 
@@ -3171,7 +3168,6 @@ lean::dec(x_1);
 return x_4;
 }
 }
-}
 obj* l_RBNode_find___main___at_Lean_getElaboratorStrategy___spec__2___boxed(obj* x_1, obj* x_2) {
 _start:
 {

src/stage0/init/lean/eqncompiler/matchpattern.cpp

@@ -14,9 +14,7 @@ typedef lean::uint32 uint32; typedef lean::uint64 uint64;
 #pragma GCC diagnostic ignored "-Wunused-label"
 #pragma GCC diagnostic ignored "-Wunused-but-set-variable"
 #endif
-namespace lean {
-uint8 has_match_pattern_attribute_core(obj*, obj*);
-}
+extern "C" uint8 lean_has_match_pattern_attribute(obj*, obj*);
 obj* l_Lean_EqnCompiler_matchPatternAttr;
 obj* l_Lean_EqnCompiler_mkMatchPatternAttr___closed__3;
 extern obj* l_Lean_TagAttribute_Inhabited___closed__3;
@@ -104,8 +102,7 @@ lean::dec(x_1);
 return x_3;
 }
 }
-namespace lean {
-uint8 has_match_pattern_attribute_core(obj* x_1, obj* x_2) {
+uint8 lean_has_match_pattern_attribute(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; uint8 x_4; 
@@ -116,12 +113,11 @@ lean::dec(x_1);
 return x_4;
 }
 }
-}
 obj* l_Lean_EqnCompiler_hasMatchPatternAttribute___boxed(obj* x_1, obj* x_2) {
 _start:
 {
 uint8 x_3; obj* x_4; 
-x_3 = lean::has_match_pattern_attribute_core(x_1, x_2);
+x_3 = lean_has_match_pattern_attribute(x_1, x_2);
 x_4 = lean::box(x_3);
 return x_4;
 }

src/stage0/init/lean/parser/module.cpp

@@ -31,9 +31,7 @@ obj* l___private_init_lean_parser_module_1__mkErrorMessage(obj*, obj*, obj*);
 obj* l_Lean_Parser_symbolInfo(obj*, obj*);
 obj* l_Lean_Parser_Module_prelude___elambda__1___rarg___closed__2;
 obj* l_Array_back___at___private_init_lean_parser_parser_6__updateCache___spec__1(obj*);
-namespace lean {
-obj* test_module_parser_core(obj*, obj*, obj*, uint8, obj*);
-}
+extern "C" obj* lean_test_module_parser(obj*, obj*, obj*, uint8, obj*);
 obj* l_Lean_Parser_manyAux___main___at_Lean_Parser_Module_header___elambda__1___spec__1(uint8, obj*, obj*, obj*);
 obj* l_Lean_Parser_andthenInfo(obj*, obj*);
 extern obj* l_Lean_Parser_declareLeadingBuiltinParser___closed__1;
@@ -2450,8 +2448,7 @@ lean::closure_set(x_2, 0, x_1);
 return x_2;
 }
 }
-namespace lean {
-obj* test_module_parser_core(obj* x_1, obj* x_2, obj* x_3, uint8 x_4, obj* x_5) {
+obj* lean_test_module_parser(obj* x_1, obj* x_2, obj* x_3, uint8 x_4, obj* x_5) {
 _start:
 {
 obj* x_6; obj* x_7; obj* x_8; obj* x_9; obj* x_10; obj* x_11; obj* x_12; obj* x_13; obj* x_14; obj* x_15; 
@@ -2505,7 +2502,6 @@ return x_21;
 }
 }
 }
-}
 obj* l_Lean_Parser_testModuleParser___lambda__1___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6, obj* x_7) {
 _start:
 {
@@ -2523,7 +2519,7 @@ _start:
 uint8 x_6; obj* x_7; 
 x_6 = lean::unbox(x_4);
 lean::dec(x_4);
-x_7 = lean::test_module_parser_core(x_1, x_2, x_3, x_6, x_5);
+x_7 = lean_test_module_parser(x_1, x_2, x_3, x_6, x_5);
 return x_7;
 }
 }

src/stage0/init/lean/path.cpp

@@ -74,9 +74,7 @@ obj* l_IO_appPath___at_Lean_getBuiltinSearchPath___spec__2(obj*);
 namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
-namespace lean {
-obj* module_name_of_file_core(obj*, obj*);
-}
+extern "C" obj* lean_module_name_of_file(obj*, obj*);
 obj* l_String_drop(obj*, obj*);
 extern obj* l_Char_HasRepr___closed__1;
 obj* l_List_reprAux___main___at_Lean_findAtSearchPath___spec__3___boxed(obj*, obj*);
@@ -126,9 +124,7 @@ obj* l___private_init_lean_path_1__pathSep;
 obj* l_Lean_findFile___boxed(obj*, obj*, obj*);
 obj* l_Array_mfindAux___main___at_Lean_findAtSearchPath___spec__1(obj*, obj*, obj*);
 obj* l_Lean_getSearchPathFromEnv(obj*);
-namespace lean {
-obj* init_search_path_core(obj*, obj*);
-}
+extern "C" obj* lean_init_search_path(obj*, obj*);
 extern uint32 l_System_FilePath_pathSeparator;
 extern obj* l_Lean_Name_toString___closed__1;
 obj* l_Array_mfindAux___main___at_Lean_findFile___spec__2___closed__2;
@@ -140,9 +136,7 @@ namespace lean {
 obj* string_utf8_byte_size(obj*);
 }
 obj* l_Array_mfindAux___main___at_Lean_findFile___spec__2(obj*, obj*, obj*, obj*, obj*);
-namespace lean {
-obj* find_lean_core(obj*, obj*);
-}
+extern "C" obj* lean_find_lean(obj*, obj*);
 obj* l_Lean_addRel(obj*, obj*);
 obj* l_String_quote(obj*);
 obj* l_Lean_mkSearchPathRef(obj*);
@@ -1797,8 +1791,7 @@ lean::dec(x_1);
 return x_3;
 }
 }
-namespace lean {
-obj* init_search_path_core(obj* x_1, obj* x_2) {
+obj* lean_init_search_path(obj* x_1, obj* x_2) {
 _start:
 {
 if (lean::obj_tag(x_1) == 0)
@@ -1969,7 +1962,6 @@ return x_41;
 }
 }
 }
-}
 obj* l_IO_fileExists___at_Lean_findFile___spec__1(obj* x_1, obj* x_2) {
 _start:
 {
@@ -2580,8 +2572,7 @@ x_4 = l_Lean_findLeanFile(x_1, x_3, x_2);
 return x_4;
 }
 }
-namespace lean {
-obj* find_lean_core(obj* x_1, obj* x_2) {
+obj* lean_find_lean(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; obj* x_4; 
@@ -2590,7 +2581,6 @@ x_4 = l_Lean_findLeanFile(x_1, x_3, x_2);
 return x_4;
 }
 }
-}
 obj* l_Array_mfindAux___main___at_Lean_findAtSearchPath___spec__1(obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
@@ -3053,8 +3043,7 @@ x_1 = lean::mk_string("' resolves to '");
 return x_1;
 }
 }
-namespace lean {
-obj* module_name_of_file_core(obj* x_1, obj* x_2) {
+obj* lean_module_name_of_file(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; 
@@ -3590,7 +3579,6 @@ return x_162;
 }
 }
 }
-}
 obj* initialize_init_system_io(obj*);
 obj* initialize_init_system_filepath(obj*);
 obj* initialize_init_data_array_default(obj*);

src/stage0/init/lean/projfns.cpp

@@ -90,16 +90,12 @@ obj* l_Lean_addProjectionFnInfo___boxed(obj*, obj*, obj*, obj*, obj*, obj*);
 obj* l_EState_bind___rarg(obj*, obj*, obj*);
 obj* l_Array_binSearchAux___main___at_Lean_Environment_isProjectionFn___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_projectionFnInfoExt___closed__5;
-namespace lean {
-obj* add_projection_info_core(obj*, obj*, obj*, obj*, obj*, uint8);
-}
+extern "C" obj* lean_add_projection_info(obj*, obj*, obj*, obj*, obj*, uint8);
 obj* l_Lean_PersistentEnvExtension_addEntry___rarg(obj*, obj*, obj*);
 obj* l_IO_Prim_Ref_get(obj*, obj*, obj*);
 uint8 l_Lean_Name_quickLt(obj*, obj*);
 obj* l_Lean_registerSimplePersistentEnvExtension___at_Lean_mkProjectionFnInfoExtension___spec__3(obj*, obj*);
-namespace lean {
-obj* get_projection_info_core(obj*, obj*);
-}
+extern "C" obj* lean_get_projection_info(obj*, obj*);
 obj* l_Array_size(obj*, obj*);
 uint8 l_Array_anyMAux___main___at_Lean_mkProjectionFnInfoExtension___spec__5(obj*, obj*, obj*);
 obj* l_Array_get(obj*, obj*, obj*, obj*);
@@ -2406,8 +2402,7 @@ lean::dec(x_1);
 return x_2;
 }
 }
-namespace lean {
-obj* add_projection_info_core(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, uint8 x_6) {
+obj* lean_add_projection_info(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, uint8 x_6) {
 _start:
 {
 obj* x_7; obj* x_8; obj* x_9; obj* x_10; 
@@ -2424,14 +2419,13 @@ x_10 = l_Lean_PersistentEnvExtension_addEntry___rarg(x_9, x_1, x_8);
 return x_10;
 }
 }
-}
 obj* l_Lean_addProjectionFnInfo___boxed(obj* x_1, obj* x_2, obj* x_3, obj* x_4, obj* x_5, obj* x_6) {
 _start:
 {
 uint8 x_7; obj* x_8; 
 x_7 = lean::unbox(x_6);
 lean::dec(x_6);
-x_8 = lean::add_projection_info_core(x_1, x_2, x_3, x_4, x_5, x_7);
+x_8 = lean_add_projection_info(x_1, x_2, x_3, x_4, x_5, x_7);
 return x_8;
 }
 }
@@ -2559,8 +2553,7 @@ goto _start;
 }
 }
 }
-namespace lean {
-obj* get_projection_info_core(obj* x_1, obj* x_2) {
+obj* lean_get_projection_info(obj* x_1, obj* x_2) {
 _start:
 {
 obj* x_3; 
@@ -2635,7 +2628,6 @@ return x_23;
 }
 }
 }
-}
 obj* l_RBNode_find___main___at_Lean_Environment_getProjectionFnInfo___spec__1___boxed(obj* x_1, obj* x_2) {
 _start:
 {

src/stage0/init/system/io.cpp

@@ -19,9 +19,7 @@ extern "C" obj* lean_io_prim_handle_get_line(obj*, obj*);
 obj* l_IO_println(obj*);
 obj* l_IO_Ref_set___boxed(obj*, obj*);
 obj* l_IO_Fs_handle_isEof___at_IO_Fs_handle_readToEnd___spec__1___boxed(obj*, obj*);
-namespace lean {
-obj* io_error_to_string_core(obj*);
-}
+extern "C" obj* lean_io_error_to_string(obj*);
 obj* l_IO_Ref_get___rarg(obj*, obj*, obj*);
 obj* l_EState_Monad(obj*, obj*);
 obj* l_IO_Ref_swap___boxed(obj*, obj*);
@@ -352,14 +350,12 @@ lean::dec(x_1);
 return x_2;
 }
 }
-namespace lean {
-obj* io_error_to_string_core(obj* x_1) {
+obj* lean_io_error_to_string(obj* x_1) {
 _start:
 {
 return x_1;
 }
 }
-}
 obj* l_unsafeIO___rarg(obj* x_1) {
 _start:
 {

src/util/io.h

@@ -10,14 +10,14 @@ Author: Leonardo de Moura
 #include "util/string_ref.h"
 
 namespace lean {
-object* io_error_to_string_core(object * err);
+extern "C" object* lean_io_error_to_string(object * err);
 
 template<typename T> T get_io_result(object * o) {
     if (io_result_is_error(o)) {
         object * err_obj = io_result_get_error(o);
         inc(err_obj);
         dec(o);
-        string_ref error(io_error_to_string_core(err_obj));
+        string_ref error(lean_io_error_to_string(err_obj));
         throw exception(error.to_std_string());
     } else {
         T r(io_result_get_value(o), true);
@@ -31,7 +31,7 @@ inline void consume_io_result(object * o) {
         object * err_obj = io_result_get_error(o);
         inc(err_obj);
         dec(o);
-        string_ref error(io_error_to_string_core(err_obj));
+        string_ref error(lean_io_error_to_string(err_obj));
         throw exception(error.to_std_string());
     }
     dec(o);
@@ -42,7 +42,7 @@ template<typename T> T get_io_scalar_result(object * o) {
         object * err_obj = io_result_get_error(o);
         inc(err_obj);
         dec(o);
-        string_ref error(io_error_to_string_core(err_obj));
+        string_ref error(lean_io_error_to_string(err_obj));
         throw exception(error.to_std_string());
     } else {
         T r = unbox(io_result_get_value(o));