diff --git a/library/init/lean/compiler/ir/compilerm.lean b/library/init/lean/compiler/ir/compilerm.lean
index 4711ca2ae3..6b53009908 100644
--- a/library/init/lean/compiler/ir/compilerm.lean
+++ b/library/init/lean/compiler/ir/compilerm.lean
@@ -26,10 +26,13 @@ end LogEntry
 
 abbrev Log := Array LogEntry
 
-@[export lean.ir.format_log_core]
-def formatLog (log : Log) : Format :=
+def Log.format (log : Log) : Format :=
 log.foldl (λ fmt entry, fmt ++ Format.line ++ format entry) Format.nil
 
+@[export lean.ir.log_to_string_core]
+def Log.toString (log : Log) : String :=
+log.format.pretty
+
 structure CompilerState :=
 (env : Environment) (log : Log := Array.empty)
 
diff --git a/src/library/compiler/compiler.cpp b/src/library/compiler/compiler.cpp
index e1beff7df1..a451492249 100644
--- a/src/library/compiler/compiler.cpp
+++ b/src/library/compiler/compiler.cpp
@@ -240,11 +240,11 @@ environment compile(environment const & env, options const & opts, names cs) {
     ds = apply(ecse, new_env, ds);
     ds = apply(elim_dead_let, ds);
     trace_compiler(name({"compiler", "simp_app_args"}), ds);
-    /* emit C++ code. */
-    comp_decls b_ds;
-    std::tie(new_env, b_ds) = to_llnf(new_env, ds, true);
-    new_env = save_llnf_code(new_env, b_ds);
-    trace_compiler(name({"compiler", "boxed"}), b_ds);
+    /* compile IR. */
+    std::tie(new_env, ds) = to_llnf(new_env, ds, true);
+    new_env = save_llnf_code(new_env, ds);
+    trace_compiler(name({"compiler", "boxed"}), ds);
+    // new_env = compile_ir(new_env, opts, ds); // TODO(Leo)
     return new_env;
 }
 
@@ -276,6 +276,12 @@ void initialize_compiler() {
     register_trace_class({"compiler", "optimize_bytecode"});
     register_trace_class({"compiler", "code_gen"});
     register_trace_class({"compiler", "ll_infer_type"});
+    register_trace_class({"compiler", "ir"});
+    register_trace_class({"compiler", "ir", "init"});
+    register_trace_class({"compiler", "ir", "push_proj"});
+    register_trace_class({"compiler", "ir", "reset_reuse"});
+    register_trace_class({"compiler", "ir", "elim_dead"});
+    register_trace_class({"compiler", "ir", "simp_case"});
 }
 
 void finalize_compiler() {
diff --git a/src/library/compiler/ir.cpp b/src/library/compiler/ir.cpp
index e8f3bd1bd4..b72945f1ed 100644
--- a/src/library/compiler/ir.cpp
+++ b/src/library/compiler/ir.cpp
@@ -9,6 +9,7 @@ Author: Leonardo de Moura
 #include "util/nat.h"
 #include "kernel/instantiate.h"
 #include "kernel/type_checker.h"
+#include "library/trace.h"
 #include "library/compiler/util.h"
 #include "library/compiler/llnf.h"
 
@@ -38,7 +39,8 @@ extern object * mk_unreachable_core;
 object * mk_alt_core(object * n, object * cidx, object * size, object * usize, object * ssize, object * b);
 object * mk_decl_core(object * f, object * xs, uint8 ty, object * b);
 object * decl_to_string_core(object * d);
-object * test_core(object * d, object * w);
+object * compile_core(object * env, object * opts, object * decls);
+object * log_to_string_core(object * log);
 /*
 inductive IRType
 | float | uint8 | uint16 | uint32 | uint64 | usize
@@ -115,17 +117,6 @@ std::string decl_to_string(decl const & d) {
     string_ref r(decl_to_string_core(d.raw()));
     return r.to_std_string();
 }
-void test(decl const & d) {
-    inc(d.raw());
-    object * r = test_core(d.raw(), io_mk_world());
-    if (io_result_is_error(r)) {
-        io_result_show_error(r);
-        dec(r);
-        throw exception("IR test error");
-    } else {
-        dec(r);
-    }
-}
 }
 
 class to_ir_fn {
@@ -479,7 +470,38 @@ public:
     ir::decl operator()(comp_decl const & d) { return to_ir_decl(d); }
 };
 
-ir::decl to_ir_decl(environment const & env, comp_decl const & d) {
+namespace ir {
+decl to_ir_decl(environment const & env, comp_decl const & d) {
     return to_ir_fn(env)(d);
 }
+
+/*
+@[export lean.ir.compile_core]
+def compile (env : Environment) (opts : Options) (decls : Array Decl) : Log × (Except String Environment) :=
+*/
+environment compile(environment const & env, options const & opts, comp_decls const & decls) {
+    buffer<decl> ir_decls;
+    for (comp_decl const & decl : decls) {
+        ir_decls.push_back(to_ir_decl(env, decl));
+    }
+    object * r   = compile_core(env.to_obj_arg(), opts.to_obj_arg(), to_array(ir_decls));
+    object * log = cnstr_get(r, 0);
+    if (array_size(log) > 0) {
+        inc(log);
+        object * str = log_to_string_core(log);
+        tout() << string_cstr(str);
+        dec_ref(str);
+    }
+    object * v  = cnstr_get(r, 1);
+    if (cnstr_tag(v) == 0) {
+        string_ref error(cnstr_get(v, 0), true);
+        dec_ref(r);
+        throw exception(error.data());
+    } else {
+        environment new_env(cnstr_get(v, 0), true);
+        dec_ref(r);
+        return new_env;
+    }
+}
+}
 }
diff --git a/src/library/compiler/ir.h b/src/library/compiler/ir.h
index a7d46e4750..629bf18b9f 100644
--- a/src/library/compiler/ir.h
+++ b/src/library/compiler/ir.h
@@ -13,6 +13,6 @@ namespace ir {
 typedef object_ref decl;
 std::string decl_to_string(decl const & d);
 void test(decl const & d);
+environment compile(environment const & env, options const & opts, comp_decls const & decls);
 }
-ir::decl to_ir_decl(environment const & env, comp_decl const & d);
 }
diff --git a/src/library/compiler/llnf.cpp b/src/library/compiler/llnf.cpp
index a4fd348c2c..079d008255 100644
--- a/src/library/compiler/llnf.cpp
+++ b/src/library/compiler/llnf.cpp
@@ -2447,6 +2447,16 @@ pair<environment, comp_decls> to_llnf(environment const & env, comp_decls const
     return mk_pair(new_env, append(_rs, _bs));
 }
 
+environment compile_ir(environment const & env, options const & opts, comp_decls const & ds) {
+    bool unboxed = true;
+    buffer<comp_decl> new_ds;
+    for (comp_decl const & d : ds) {
+        expr new_v = to_lambda_pure_fn(env, unboxed)(d.snd());
+        new_ds.push_back(comp_decl(d.fst(), new_v));
+    }
+    return ir::compile(env, opts, new_ds);
+}
+
 void initialize_llnf() {
     g_apply     = new expr(mk_constant("_apply"));
     g_closure   = new expr(mk_constant("_closure"));
diff --git a/src/library/compiler/llnf.h b/src/library/compiler/llnf.h
index f1ffce7a29..50c1f3a079 100644
--- a/src/library/compiler/llnf.h
+++ b/src/library/compiler/llnf.h
@@ -15,6 +15,8 @@ pair<environment, comp_decls> to_llnf(environment const & env, comp_decls const
 
 optional<pair<environment, comp_decl>> mk_boxed_version(environment env, name const & fn, unsigned arity);
 
+environment compile_ir(environment const & env, options const & opts, comp_decls const & ds);
+
 bool is_llnf_apply(expr const & e);
 bool is_llnf_closure(expr const & e);
 bool is_llnf_cnstr(expr const & e, name & I, unsigned & cidx, unsigned & nusize, unsigned & ssz);
diff --git a/src/stage0/init/lean/compiler/ir/compilerm.cpp b/src/stage0/init/lean/compiler/ir/compilerm.cpp
index 3bed4a4aed..956739c034 100644
--- a/src/stage0/init/lean/compiler/ir/compilerm.cpp
+++ b/src/stage0/init/lean/compiler/ir/compilerm.cpp
@@ -28,6 +28,7 @@ obj* l_Lean_IR_containsDecl(obj*, obj*, obj*);
 obj* l_Lean_IR_LogEntry_fmt___main(obj*);
 extern obj* l_Array_empty___closed__1;
 obj* l_Lean_IR_logMessage___boxed(obj*);
+obj* l_Lean_Format_pretty(obj*, obj*);
 obj* l_Lean_IR_mkDeclMapExtension___closed__1;
 extern obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__2;
 obj* l___private_init_lean_compiler_ir_compilerm_3__logMessageIfAux___boxed(obj*);
@@ -41,6 +42,7 @@ obj* l_HashMapImp_insert___at___private_init_lean_compiler_ir_compilerm_4__mkEnt
 obj* l_mkHashMap___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__1(obj*);
 obj* l___private_init_lean_compiler_ir_compilerm_2__logDeclsAux(obj*, obj*, obj*, obj*, obj*);
 obj* l_HashMapImp_find___at_Lean_IR_findDecl___spec__3(obj*, obj*);
+obj* l_Lean_IR_Log_format(obj*);
 obj* l_Lean_IR_logMessage___rarg___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_AssocList_foldl___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__6(obj*, obj*);
 obj* l_Lean_IR_findDecl(obj*, obj*, obj*);
@@ -51,6 +53,8 @@ extern obj* l_Lean_Format_sbracket___closed__1;
 obj* l_Array_miterateAux___main___at_Lean_IR_LogEntry_fmt___main___spec__1(obj*, obj*, obj*, obj*);
 obj* l_List_redLength___main___rarg(obj*);
 obj* l_Lean_IR_addDecls___boxed(obj*, obj*, obj*);
+extern obj* l_Lean_Options_empty;
+obj* l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1(obj*, obj*, obj*, obj*);
 uint8 l_Lean_SMap_contains___main___at_Lean_IR_containsDecl___spec__1(obj*, obj*);
 obj* l_Lean_SMap_find___main___at_Lean_IR_findDecl___spec__1(obj*, obj*);
 obj* l_HashMapImp_expand___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__4(obj*, obj*);
@@ -78,6 +82,10 @@ obj* l_Lean_SMap_switch___at_Lean_IR_mkDeclMapExtension___spec__2(obj*);
 obj* l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___closed__1;
 obj* l_Lean_IR_addDecls(obj*, obj*, obj*);
 namespace lean {
+namespace ir {
+obj* log_to_string_core(obj*);
+}}
+namespace lean {
 uint8 nat_dec_lt(obj*, obj*);
 }
 obj* l_Array_miterateAux___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__10___boxed(obj*, obj*, obj*, obj*);
@@ -92,7 +100,6 @@ obj* l_Lean_IR_Decl_name___main(obj*);
 obj* l_Lean_IR_declMapExt___elambda__2(uint8);
 obj* l_Lean_IR_LogEntry_Lean_HasFormat;
 obj* l_Lean_IR_findDecl___boxed(obj*, obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_formatLog___spec__1(obj*, obj*, obj*, obj*);
 namespace lean {
 obj* nat_add(obj*, obj*);
 }
@@ -106,6 +113,7 @@ uint8 l_AssocList_contains___main___at___private_init_lean_compiler_ir_compilerm
 obj* l_Array_mforAux___main___at_Lean_IR_addDecls___spec__1(obj*, obj*, obj*, obj*);
 uint8 l___private_init_lean_compiler_ir_compilerm_1__isLogEnabledFor(obj*, obj*);
 obj* l_RBNode_ins___main___at_Lean_IR_mkDeclMapExtension___spec__5(obj*, obj*, obj*);
+obj* l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1___boxed(obj*, obj*, obj*, obj*);
 obj* l_Lean_IR_declMapExt___elambda__1(obj*);
 extern obj* l_Lean_SMap_insert___main___at_Lean_Environment_add___spec__1___closed__2;
 obj* l___private_init_lean_compiler_ir_compilerm_4__mkEntryArray(obj*);
@@ -118,10 +126,6 @@ namespace lean {
 usize usize_modn(usize, obj*);
 }
 obj* l_HashMapImp_find___at_Lean_IR_findDecl___spec__3___boxed(obj*, obj*);
-namespace lean {
-namespace ir {
-obj* format_log_core(obj*);
-}}
 obj* l___private_init_lean_compiler_ir_compilerm_2__logDeclsAux___boxed(obj*, obj*, obj*, obj*, obj*);
 obj* l_mkHashMapImp___rarg(obj*);
 obj* l_Lean_IR_modifyEnv(obj*, obj*, obj*);
@@ -130,6 +134,7 @@ obj* l___private_init_lean_compiler_ir_compilerm_3__logMessageIfAux___rarg(obj*,
 uint8 l_HashMapImp_contains___at_Lean_IR_containsDecl___spec__2(obj*, obj*);
 obj* l_Lean_IR_declMapExt___elambda__2___rarg(obj*, obj*);
 extern obj* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
+obj* l_Lean_IR_Log_format___boxed(obj*);
 extern obj* l_Lean_Name_toString___closed__1;
 obj* l_Lean_IR_log___boxed(obj*, obj*, obj*);
 namespace lean {
@@ -142,7 +147,6 @@ obj* l_AssocList_find___main___at_Lean_IR_findDecl___spec__4___boxed(obj*, obj*)
 obj* l_List_foldl___main___at___private_init_lean_compiler_ir_compilerm_4__mkEntryArray___spec__8___boxed(obj*, obj*, obj*);
 obj* l_Lean_IR_addDecl(obj*, obj*, obj*);
 obj* l_Lean_Name_append___main(obj*, obj*);
-obj* l_Array_miterateAux___main___at_Lean_IR_formatLog___spec__1___boxed(obj*, obj*, obj*, obj*);
 namespace lean {
 obj* nat_mul(obj*, obj*);
 }
@@ -271,7 +275,7 @@ x_0 = lean::alloc_closure(reinterpret_cast<void*>(l_Lean_IR_LogEntry_fmt), 1, 0)
 return x_0;
 }
 }
-obj* l_Array_miterateAux___main___at_Lean_IR_formatLog___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; uint8 x_5; 
@@ -309,30 +313,51 @@ goto _start;
 }
 }
 }
-namespace lean {
-namespace ir {
-obj* format_log_core(obj* x_0) {
+obj* l_Lean_IR_Log_format(obj* x_0) {
 _start:
 {
 obj* x_1; obj* x_2; obj* x_3; 
 x_1 = lean::mk_nat_obj(0ul);
 x_2 = lean::box(0);
-x_3 = l_Array_miterateAux___main___at_Lean_IR_formatLog___spec__1(x_0, x_0, x_1, x_2);
-lean::dec(x_0);
+x_3 = l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1(x_0, x_0, x_1, x_2);
 return x_3;
 }
 }
-}}
-obj* l_Array_miterateAux___main___at_Lean_IR_formatLog___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
+obj* l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1___boxed(obj* x_0, obj* x_1, obj* x_2, obj* x_3) {
 _start:
 {
 obj* x_4; 
-x_4 = l_Array_miterateAux___main___at_Lean_IR_formatLog___spec__1(x_0, x_1, x_2, x_3);
+x_4 = l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1(x_0, x_1, x_2, x_3);
 lean::dec(x_0);
 lean::dec(x_1);
 return x_4;
 }
 }
+obj* l_Lean_IR_Log_format___boxed(obj* x_0) {
+_start:
+{
+obj* x_1; 
+x_1 = l_Lean_IR_Log_format(x_0);
+lean::dec(x_0);
+return x_1;
+}
+}
+namespace lean {
+namespace ir {
+obj* log_to_string_core(obj* x_0) {
+_start:
+{
+obj* x_1; obj* x_2; obj* x_3; obj* x_5; obj* x_6; 
+x_1 = lean::mk_nat_obj(0ul);
+x_2 = lean::box(0);
+x_3 = l_Array_miterateAux___main___at_Lean_IR_Log_format___spec__1(x_0, x_0, x_1, x_2);
+lean::dec(x_0);
+x_5 = l_Lean_Options_empty;
+x_6 = l_Lean_Format_pretty(x_3, x_5);
+return x_6;
+}
+}
+}}
 obj* l_Lean_IR_log(obj* x_0, obj* x_1, obj* x_2) {
 _start:
 {