more

Author: hargoniX

src/include/lean/lean.h

@@ -2831,17 +2831,17 @@ static inline lean_obj_res lean_io_mk_world() { return lean_box(0); }
 
 static inline b_lean_obj_res lean_baseio_out_val(b_lean_obj_arg r) {
     // TODO: This function needs to become identity after we are done.
-    return lean_ctor_get(r, 0);
-    // return r;
+    // return lean_ctor_get(r, 0);
+    return r;
 }
 
 static inline lean_obj_res lean_mk_baseio_out(lean_obj_arg i) {
     // TODO: This function needs to become identity after we are done.
-    lean_object * r = lean_alloc_ctor(0, 2, 0);
-    lean_ctor_set(r, 0, i);
-    lean_ctor_set(r, 1, lean_box(0));
-    return r;
+    // lean_object * r = lean_alloc_ctor(0, 2, 0);
+    // lean_ctor_set(r, 0, i);
+    // lean_ctor_set(r, 1, lean_box(0));
     // return r;
+    return i;
 }
 
 static inline bool lean_io_result_is_ok(b_lean_obj_arg r) {

src/library/ir_interpreter.cpp

@@ -1153,9 +1153,9 @@ uint32 run_main(elab_environment const & env, options const & opts, list_ref<str
 }
 
 /* runMain (env : Environment) (opts : Iptions) (args : List String) : BaseIO UInt32 */
-extern "C" LEAN_EXPORT obj_res lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args, obj_arg) {
+extern "C" LEAN_EXPORT uint32_t lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args, obj_arg) {
     uint32 ret = run_main(TO_REF(elab_environment, env), TO_REF(options, opts), TO_REF(list_ref<string_ref>, args));
-    return lean_mk_baseio_out(box(ret));
+    return ret;
 }
 
 extern "C" LEAN_EXPORT object * lean_eval_const(object * env, object * opts, object * c) {