chore: update stage0

stage0/src/Lean/Compiler/IR.lean

@@ -20,6 +20,7 @@ import Lean.Compiler.IR.UnboxResult
 import Lean.Compiler.IR.ElimDeadBranches
 import Lean.Compiler.IR.EmitC
 import Lean.Compiler.IR.CtorLayout
+import Lean.Compiler.IR.Sorry
 
 namespace Lean.IR
 
@@ -47,6 +48,7 @@ private def compileAux (decls : Array Decl) : CompilerM Unit := do
   logDecls `expand_reset_reuse decls
   let decls := decls.map Decl.pushProj
   logDecls `push_proj decls
+  let decls ← updateSorryDep decls
   logDecls `result decls
   checkDecls decls
   addDecls decls

stage0/src/Lean/Compiler/IR/CompilerM.lean

@@ -142,5 +142,11 @@ def getDecl' (n : Name) (decls : Array Decl) : CompilerM Decl := do
   let (some decl) ← findDecl' n decls | throw s!"unknown declaration '{n}'"
   pure decl
 
+@[export lean_decl_get_sorry_dep]
+def getSorryDep (env : Environment) (declName : Name) : Option Name :=
+  match (declMapExt.getState env).find? declName with
+  | some (Decl.fdecl (info := { sorryDep? := dep?, .. }) ..) => dep?
+  | _ => none
+
 end IR
 end Lean

stage0/src/Lean/Compiler/IR/Sorry.lean

@@ -0,0 +1,79 @@
+/-
+Copyright (c) 2021 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+import Lean.Compiler.IR.CompilerM
+
+namespace Lean.IR
+namespace Sorry
+
+structure State where
+  localSorryMap : NameMap Name := {}
+  modified : Bool := false
+
+abbrev M := StateT State CompilerM
+
+def visitExpr : Expr → ExceptT Name M Unit
+  | Expr.fap f _  => getSorryDepFor? f
+  | Expr.pap f _  => getSorryDepFor? f
+  | _             => return ()
+where
+  getSorryDepFor? (f : Name) : ExceptT Name M Unit := do
+    let found (g : Name) :=
+      if g == ``sorryAx then
+        throw f
+      else
+        throw g
+    if f == ``sorryAx then
+      throw f
+    else if let some g := (← get).localSorryMap.find? f then
+      found g
+    else match (← findDecl f) with
+      | Decl.fdecl (info := { sorryDep? := some g, .. }) .. => found g
+      | _ => return ()
+
+partial def visitFndBody (b : FnBody) : ExceptT Name M Unit := do
+  match b with
+  | FnBody.vdecl _ _ v b   => visitExpr v; visitFndBody b
+  | FnBody.jdecl _ _ v b   => visitFndBody v; visitFndBody b
+  | FnBody.case _ _ _ alts => alts.forM fun alt => visitFndBody alt.body
+  | _ =>
+    unless b.isTerminal do
+      let (instr, b) := b.split
+      visitFndBody b
+
+def visitDecl (d : Decl) : M Unit := do
+  match d with
+  | Decl.fdecl (f := f) (body := b) .. =>
+    match (← get).localSorryMap.find? f with
+    | some _ => return ()
+    | none =>
+      match (← visitFndBody b |>.run) with
+      | Except.ok _    => return ()
+      | Except.error g =>
+        modify fun s => {
+          localSorryMap := s.localSorryMap.insert f g
+          modified      := true
+        }
+  | _ => return ()
+
+partial def collect (decls : Array Decl) : M Unit := do
+  modify fun s => { s with modified := false }
+  decls.forM visitDecl
+  if (← get).modified then
+    collect decls
+
+end Sorry
+
+def updateSorryDep (decls : Array Decl) : CompilerM (Array Decl) := do
+  let (_, s) ← Sorry.collect decls |>.run {}
+  return decls.map fun decl =>
+    match decl with
+    | Decl.fdecl f xs t b info =>
+      match s.localSorryMap.find? f with
+      | some g => Decl.fdecl f xs t b { info with sorryDep? := some g }
+      | _ => decl
+    | _ => decl
+
+end Lean.IR

stage0/src/library/compiler/ir_interpreter.cpp

@@ -1004,7 +1004,16 @@ public:
     }
 };
 
+extern "C" object * lean_decl_get_sorry_dep(object * env, object * n);
+
+optional<name> get_sorry_dep(environment const & env, name const & n) {
+    return option_ref<name>(lean_decl_get_sorry_dep(env.to_obj_arg(), n.to_obj_arg())).get();
+}
+
 object * run_boxed(environment const & env, options const & opts, name const & fn, unsigned n, object **args) {
+    if (get_sorry_dep(env, fn)) {
+        throw exception("cannot evaluate code because it uses 'sorry' and/or contains errors");
+    }
     return interpreter::with_interpreter<object *>(env, opts, [&](interpreter & interp) { return interp.call_boxed(fn, n, args); });
 }
 uint32 run_main(environment const & env, options const & opts, int argv, char * argc[]) {

stage0/stdlib/Lean/Compiler/IR.c

@@ -1,6 +1,6 @@
 // Lean compiler output
 // Module: Lean.Compiler.IR
-// Imports: Init Lean.Compiler.IR.Basic Lean.Compiler.IR.Format Lean.Compiler.IR.CompilerM Lean.Compiler.IR.PushProj Lean.Compiler.IR.ElimDeadVars Lean.Compiler.IR.SimpCase Lean.Compiler.IR.ResetReuse Lean.Compiler.IR.NormIds Lean.Compiler.IR.Checker Lean.Compiler.IR.Borrow Lean.Compiler.IR.Boxing Lean.Compiler.IR.RC Lean.Compiler.IR.ExpandResetReuse Lean.Compiler.IR.UnboxResult Lean.Compiler.IR.ElimDeadBranches Lean.Compiler.IR.EmitC Lean.Compiler.IR.CtorLayout
+// Imports: Init Lean.Compiler.IR.Basic Lean.Compiler.IR.Format Lean.Compiler.IR.CompilerM Lean.Compiler.IR.PushProj Lean.Compiler.IR.ElimDeadVars Lean.Compiler.IR.SimpCase Lean.Compiler.IR.ResetReuse Lean.Compiler.IR.NormIds Lean.Compiler.IR.Checker Lean.Compiler.IR.Borrow Lean.Compiler.IR.Boxing Lean.Compiler.IR.RC Lean.Compiler.IR.ExpandResetReuse Lean.Compiler.IR.UnboxResult Lean.Compiler.IR.ElimDeadBranches Lean.Compiler.IR.EmitC Lean.Compiler.IR.CtorLayout Lean.Compiler.IR.Sorry
 #include <lean/lean.h>
 #if defined(__clang__)
 #pragma clang diagnostic ignored "-Wunused-parameter"
@@ -76,6 +76,7 @@ lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__2;
 lean_object* l_Lean_IR_Decl_simpCase(lean_object*);
 lean_object* l_Lean_IR_Decl_expandResetReuse(lean_object*);
 lean_object* l_Lean_IR_elimDeadBranches(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_updateSorryDep(lean_object*, lean_object*, lean_object*);
 lean_object* l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__21;
 lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Compiler_IR_0__Lean_IR_compileAux___spec__5(size_t, size_t, lean_object*);
 uint8_t lean_nat_dec_le(lean_object*, lean_object*);
@@ -583,7 +584,7 @@ lean_inc(x_1);
 x_8 = l_Lean_IR_checkDecls(x_1, x_2, x_7);
 if (lean_obj_tag(x_8) == 0)
 {
-lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; size_t x_18; size_t x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; size_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; size_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; size_t x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; size_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; size_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; size_t x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; 
+lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; size_t x_18; size_t x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; size_t x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; size_t x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; size_t x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; size_t x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64; lean_object* x_65; lean_object* x_66; lean_object* x_67; lean_object* x_68; lean_object* x_69; lean_object* x_70; lean_object* x_71; lean_object* x_72; lean_object* x_73; lean_object* x_74; lean_object* x_75; lean_object* x_76; lean_object* x_77; lean_object* x_78; lean_object* x_79; lean_object* x_80; size_t x_81; lean_object* x_82; lean_object* x_83; lean_object* x_84; lean_object* x_85; lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89; size_t x_90; lean_object* x_91; lean_object* x_92; lean_object* x_93; lean_object* x_94; lean_object* x_95; lean_object* x_96; lean_object* x_97; lean_object* x_98; lean_object* x_99; lean_object* x_100; lean_object* x_101; lean_object* x_102; lean_object* x_103; 
 x_9 = lean_ctor_get(x_8, 1);
 lean_inc(x_9);
 lean_dec(x_8);
@@ -722,70 +723,76 @@ x_94 = l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux(x_23, x_24,
 x_95 = lean_ctor_get(x_94, 1);
 lean_inc(x_95);
 lean_dec(x_94);
-x_96 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__31;
-x_97 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__30;
-lean_inc(x_93);
-x_98 = l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux(x_96, x_97, x_93, x_2, x_95);
-x_99 = lean_ctor_get(x_98, 1);
-lean_inc(x_99);
-lean_dec(x_98);
-lean_inc(x_93);
-x_100 = l_Lean_IR_checkDecls(x_93, x_2, x_99);
-if (lean_obj_tag(x_100) == 0)
+x_96 = l_Lean_IR_updateSorryDep(x_93, x_2, x_95);
+x_97 = lean_ctor_get(x_96, 0);
+lean_inc(x_97);
+x_98 = lean_ctor_get(x_96, 1);
+lean_inc(x_98);
+lean_dec(x_96);
+x_99 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__31;
+x_100 = l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__30;
+lean_inc(x_97);
+x_101 = l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux(x_99, x_100, x_97, x_2, x_98);
+x_102 = lean_ctor_get(x_101, 1);
+lean_inc(x_102);
+lean_dec(x_101);
+lean_inc(x_97);
+x_103 = l_Lean_IR_checkDecls(x_97, x_2, x_102);
+if (lean_obj_tag(x_103) == 0)
 {
-lean_object* x_101; lean_object* x_102; 
-x_101 = lean_ctor_get(x_100, 1);
-lean_inc(x_101);
-lean_dec(x_100);
-x_102 = l_Lean_IR_addDecls(x_93, x_2, x_101);
-lean_dec(x_93);
-return x_102;
-}
-else
-{
-uint8_t x_103; 
-lean_dec(x_93);
-x_103 = !lean_is_exclusive(x_100);
-if (x_103 == 0)
-{
-return x_100;
-}
-else
-{
-lean_object* x_104; lean_object* x_105; lean_object* x_106; 
-x_104 = lean_ctor_get(x_100, 0);
-x_105 = lean_ctor_get(x_100, 1);
-lean_inc(x_105);
+lean_object* x_104; lean_object* x_105; 
+x_104 = lean_ctor_get(x_103, 1);
 lean_inc(x_104);
-lean_dec(x_100);
-x_106 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_106, 0, x_104);
-lean_ctor_set(x_106, 1, x_105);
-return x_106;
+lean_dec(x_103);
+x_105 = l_Lean_IR_addDecls(x_97, x_2, x_104);
+lean_dec(x_97);
+return x_105;
+}
+else
+{
+uint8_t x_106; 
+lean_dec(x_97);
+x_106 = !lean_is_exclusive(x_103);
+if (x_106 == 0)
+{
+return x_103;
+}
+else
+{
+lean_object* x_107; lean_object* x_108; lean_object* x_109; 
+x_107 = lean_ctor_get(x_103, 0);
+x_108 = lean_ctor_get(x_103, 1);
+lean_inc(x_108);
+lean_inc(x_107);
+lean_dec(x_103);
+x_109 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_109, 0, x_107);
+lean_ctor_set(x_109, 1, x_108);
+return x_109;
 }
 }
 }
 else
 {
-uint8_t x_107; 
+uint8_t x_110; 
 lean_dec(x_1);
-x_107 = !lean_is_exclusive(x_8);
-if (x_107 == 0)
+x_110 = !lean_is_exclusive(x_8);
+if (x_110 == 0)
 {
 return x_8;
 }
 else
 {
-lean_object* x_108; lean_object* x_109; lean_object* x_110; 
-x_108 = lean_ctor_get(x_8, 0);
-x_109 = lean_ctor_get(x_8, 1);
-lean_inc(x_109);
-lean_inc(x_108);
+lean_object* x_111; lean_object* x_112; lean_object* x_113; 
+x_111 = lean_ctor_get(x_8, 0);
+x_112 = lean_ctor_get(x_8, 1);
+lean_inc(x_112);
+lean_inc(x_111);
 lean_dec(x_8);
-x_110 = lean_alloc_ctor(1, 2, 0);
-lean_ctor_set(x_110, 0, x_108);
-lean_ctor_set(x_110, 1, x_109);
-return x_110;
+x_113 = lean_alloc_ctor(1, 2, 0);
+lean_ctor_set(x_113, 0, x_111);
+lean_ctor_set(x_113, 1, x_112);
+return x_113;
 }
 }
 }
@@ -1384,6 +1391,7 @@ lean_object* initialize_Lean_Compiler_IR_UnboxResult(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_ElimDeadBranches(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_EmitC(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_CtorLayout(lean_object*);
+lean_object* initialize_Lean_Compiler_IR_Sorry(lean_object*);
 static bool _G_initialized = false;
 lean_object* initialize_Lean_Compiler_IR(lean_object* w) {
 lean_object * res;
@@ -1443,6 +1451,9 @@ lean_dec_ref(res);
 res = initialize_Lean_Compiler_IR_CtorLayout(lean_io_mk_world());
 if (lean_io_result_is_error(res)) return res;
 lean_dec_ref(res);
+res = initialize_Lean_Compiler_IR_Sorry(lean_io_mk_world());
+if (lean_io_result_is_error(res)) return res;
+lean_dec_ref(res);
 l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__1 = _init_l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__1();
 lean_mark_persistent(l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__1);
 l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__2 = _init_l___private_Lean_Compiler_IR_0__Lean_IR_compileAux___closed__2();

stage0/stdlib/Lean/Compiler/IR/CompilerM.c

@@ -79,6 +79,7 @@ lean_object* l_Lean_registerSimplePersistentEnvExtension___rarg___lambda__2(lean
 lean_object* lean_array_fget(lean_object*, lean_object*);
 lean_object* l_Lean_mkStateFromImportedEntries___at_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____spec__6(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_Log_format___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_getSorryDep_match__1___rarg(lean_object*, lean_object*, lean_object*);
 extern lean_object* l_Std_PersistentHashMap_insertAux___rarg___closed__3;
 lean_object* l_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____closed__4;
 uint8_t l_Lean_SMap_contains___at_Lean_IR_containsDecl___spec__1(lean_object*, lean_object*);
@@ -183,6 +184,7 @@ lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_IR_findEnvDecl___spec__2
 lean_object* l_Lean_IR_tracePrefixOptionName___closed__1;
 lean_object* l_Std_HashMapImp_find_x3f___at_Lean_IR_findEnvDecl___spec__5(lean_object*, lean_object*);
 lean_object* l_Lean_IR_findEnvDecl_x27___boxed(lean_object*, lean_object*, lean_object*);
+lean_object* l_Lean_IR_getSorryDep_match__1(lean_object*);
 lean_object* l_Lean_IR_getDecl_match__1(lean_object*);
 lean_object* l___private_Lean_Compiler_IR_CompilerM_0__Lean_IR_logDeclsAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
 lean_object* l_Lean_IR_addDecl(lean_object*, lean_object*, lean_object*);
@@ -196,6 +198,7 @@ extern size_t l_Std_PersistentHashMap_insertAux___rarg___closed__2;
 lean_object* l_Lean_IR_modifyEnv___boxed(lean_object*, lean_object*, lean_object*);
 lean_object* lean_ir_find_env_decl(lean_object*, lean_object*);
 lean_object* l_Array_foldlMUnsafe_fold___at_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____spec__8___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
+lean_object* lean_decl_get_sorry_dep(lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_insert___at_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____spec__2(lean_object*, lean_object*, lean_object*);
 lean_object* l_Std_PersistentHashMap_findAux___at_Lean_IR_findEnvDecl___spec__3(lean_object*, size_t, lean_object*);
 lean_object* l_Lean_IR_initFn____x40_Lean_Compiler_IR_CompilerM___hyg_340____lambda__2___boxed(lean_object*);
@@ -4004,6 +4007,98 @@ lean_dec(x_2);
 return x_5;
 }
 }
+lean_object* l_Lean_IR_getSorryDep_match__1___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
+_start:
+{
+if (lean_obj_tag(x_1) == 0)
+{
+lean_object* x_4; 
+lean_dec(x_2);
+x_4 = lean_apply_1(x_3, x_1);
+return x_4;
+}
+else
+{
+lean_object* x_5; 
+x_5 = lean_ctor_get(x_1, 0);
+lean_inc(x_5);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; 
+lean_dec(x_3);
+lean_dec(x_1);
+x_6 = lean_ctor_get(x_5, 0);
+lean_inc(x_6);
+x_7 = lean_ctor_get(x_5, 1);
+lean_inc(x_7);
+x_8 = lean_ctor_get(x_5, 2);
+lean_inc(x_8);
+x_9 = lean_ctor_get(x_5, 3);
+lean_inc(x_9);
+x_10 = lean_ctor_get(x_5, 4);
+lean_inc(x_10);
+lean_dec(x_5);
+x_11 = lean_apply_5(x_2, x_6, x_7, x_8, x_9, x_10);
+return x_11;
+}
+else
+{
+lean_object* x_12; 
+lean_dec(x_5);
+lean_dec(x_2);
+x_12 = lean_apply_1(x_3, x_1);
+return x_12;
+}
+}
+}
+}
+lean_object* l_Lean_IR_getSorryDep_match__1(lean_object* x_1) {
+_start:
+{
+lean_object* x_2; 
+x_2 = lean_alloc_closure((void*)(l_Lean_IR_getSorryDep_match__1___rarg), 3, 0);
+return x_2;
+}
+}
+lean_object* lean_decl_get_sorry_dep(lean_object* x_1, lean_object* x_2) {
+_start:
+{
+lean_object* x_3; lean_object* x_4; lean_object* x_5; 
+x_3 = l_Lean_IR_declMapExt;
+x_4 = l_Lean_SimplePersistentEnvExtension_getState___rarg(x_3, x_1);
+lean_dec(x_1);
+x_5 = l_Lean_SMap_find_x3f___at_Lean_IR_findEnvDecl___spec__1(x_4, x_2);
+lean_dec(x_2);
+if (lean_obj_tag(x_5) == 0)
+{
+lean_object* x_6; 
+x_6 = lean_box(0);
+return x_6;
+}
+else
+{
+lean_object* x_7; 
+x_7 = lean_ctor_get(x_5, 0);
+lean_inc(x_7);
+lean_dec(x_5);
+if (lean_obj_tag(x_7) == 0)
+{
+lean_object* x_8; 
+x_8 = lean_ctor_get(x_7, 4);
+lean_inc(x_8);
+lean_dec(x_7);
+return x_8;
+}
+else
+{
+lean_object* x_9; 
+lean_dec(x_7);
+x_9 = lean_box(0);
+return x_9;
+}
+}
+}
+}
 lean_object* initialize_Init(lean_object*);
 lean_object* initialize_Lean_Environment(lean_object*);
 lean_object* initialize_Lean_Compiler_IR_Basic(lean_object*);