refactor(library/io_state): move to the kernel

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

src/frontends/lean/frontend.cpp

@@ -18,9 +18,9 @@ Author: Leonardo de Moura
 #include "kernel/expr_maps.h"
 #include "kernel/expr_sets.h"
 #include "kernel/builtin.h"
+#include "kernel/io_state.h"
 #include "library/expr_pair.h"
 #include "library/expr_pair_maps.h"
-#include "library/io_state.h"
 #include "library/all/all.h"
 #include "frontends/lean/operator_info.h"
 #include "frontends/lean/coercion.h"

src/frontends/lean/frontend.h

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <memory>
 #include <vector>
 #include "kernel/environment.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/expr_pair.h"
 #include "frontends/lean/operator_info.h"
 

src/frontends/lean/operator_info.h

@@ -9,7 +9,7 @@ Author: Leonardo de Moura
 #include "util/name.h"
 #include "util/list.h"
 #include "util/sexpr/format.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "kernel/object.h"
 
 namespace lean {

src/frontends/lean/parser.cpp

@@ -38,9 +38,9 @@ Author: Leonardo de Moura
 #include "kernel/for_each_fn.h"
 #include "kernel/find_fn.h"
 #include "kernel/type_checker_justification.h"
+#include "kernel/io_state.h"
 #include "library/expr_lt.h"
 #include "library/arith/arith.h"
-#include "library/io_state.h"
 #include "library/placeholder.h"
 #include "library/kernel_bindings.h"
 #include "library/elaborator/elaborator_exception.h"

src/frontends/lean/parser.h

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include <iostream>
 #include "util/lua.h"
 #include "kernel/environment.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 
 namespace lean {
 class script_state;

src/frontends/lean/register_module.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "util/lua.h"
 #include "util/script_state.h"
 #include "util/sexpr/options.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/kernel_bindings.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/frontend.h"

src/kernel/CMakeLists.txt

@@ -1,8 +1,9 @@
 add_library(kernel expr.cpp free_vars.cpp abstract.cpp instantiate.cpp
   normalizer.cpp context.cpp level.cpp object.cpp environment.cpp
-  type_checker.cpp builtin.cpp occurs.cpp metavar.cpp justification.cpp
-  unification_constraint.cpp printer.cpp formatter.cpp
-  kernel_exception.cpp type_checker_justification.cpp pos_info_provider.cpp
-  replace_visitor.cpp update_expr.cpp)
+  type_checker.cpp builtin.cpp occurs.cpp metavar.cpp
+  justification.cpp unification_constraint.cpp printer.cpp
+  formatter.cpp kernel_exception.cpp type_checker_justification.cpp
+  pos_info_provider.cpp replace_visitor.cpp update_expr.cpp
+  io_state.cpp)
 
 target_link_libraries(kernel ${LEAN_LIBS})

src/kernel/io_state.cpp

@@ -0,0 +1,72 @@
+/*
+Copyright (c) 2013 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Leonardo de Moura
+*/
+#include "kernel/io_state.h"
+#include "kernel/kernel_exception.h"
+
+namespace lean {
+io_state::io_state():
+    m_formatter(mk_simple_formatter()),
+    m_regular_channel(std::make_shared<stdout_channel>()),
+    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
+}
+
+io_state::io_state(options const & opts, formatter const & fmt):
+    m_options(opts),
+    m_formatter(fmt),
+    m_regular_channel(std::make_shared<stdout_channel>()),
+    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
+}
+
+io_state::~io_state() {}
+
+void io_state::set_regular_channel(std::shared_ptr<output_channel> const & out) {
+    if (out)
+        m_regular_channel = out;
+}
+
+void io_state::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) {
+    if (out)
+        m_diagnostic_channel = out;
+}
+
+void io_state::set_options(options const & opts) {
+    m_options = opts;
+}
+
+void io_state::set_formatter(formatter const & f) {
+    m_formatter = f;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
+    out.get_stream() << std::endl;
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts);
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, object const & obj) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts);
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, environment const & env) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts);
+    return out;
+}
+
+io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) {
+    options const & opts = out.get_options();
+    out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts);
+    return out;
+}
+}

src/kernel/io_state.h

@@ -90,24 +90,4 @@ template<typename T> io_state_stream const & operator<<(io_state_stream const &
     out.get_stream() << t;
     return out;
 }
-
-UDATA_DEFS(io_state)
-/**
-   \brief Auxiliary class for temporarily setting the Lua registry of a Lua state
-   with a Lean io_state object.
-*/
-class set_io_state {
-    lua_State * m_state;
-    io_state *  m_prev;
-    options     m_prev_options;
-public:
-    set_io_state(lua_State * L, io_state & st);
-    ~set_io_state();
-};
-/**
-   \brief Return the Lean state object associated with the given Lua state.
-   Return nullptr is there is none.
-*/
-io_state * get_io_state(lua_State * L);
-void open_io_state(lua_State * L);
 }

src/library/CMakeLists.txt

@@ -1,5 +1,5 @@
 add_library(library kernel_bindings.cpp basic_thms.cpp deep_copy.cpp
-  max_sharing.cpp context_to_lambda.cpp io_state.cpp placeholder.cpp
-  expr_lt.cpp substitution.cpp fo_unify.cpp bin_op.cpp)
+  max_sharing.cpp context_to_lambda.cpp placeholder.cpp expr_lt.cpp
+  substitution.cpp fo_unify.cpp bin_op.cpp)
 
 target_link_libraries(library ${LEAN_LIBS})

src/library/arith/int.cpp

@@ -8,7 +8,7 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
 #include "kernel/value.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/kernel_bindings.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"

src/library/arith/nat.cpp

@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
 #include "kernel/value.h"
+#include "kernel/io_state.h"
 #include "library/kernel_bindings.h"
-#include "library/io_state.h"
 #include "library/arith/nat.h"
 
 namespace lean {

src/library/arith/real.cpp

@@ -8,8 +8,8 @@ Author: Leonardo de Moura
 #include "kernel/abstract.h"
 #include "kernel/environment.h"
 #include "kernel/value.h"
+#include "kernel/io_state.h"
 #include "library/kernel_bindings.h"
-#include "library/io_state.h"
 #include "library/arith/real.h"
 #include "library/arith/int.h"
 #include "library/arith/nat.h"

src/library/arith/special_fn.cpp

@@ -6,7 +6,7 @@ Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
 #include "kernel/abstract.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/arith/special_fn.h"
 #include "library/arith/real.h"
 

src/library/basic_thms.cpp

@@ -5,7 +5,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: Leonardo de Moura
 */
 #include "kernel/environment.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/basic_thms.h"
 
 namespace lean {

src/library/io_state.cpp

@@ -1,216 +0,0 @@
-/*
-Copyright (c) 2013 Microsoft Corporation. All rights reserved.
-Released under Apache 2.0 license as described in the file LICENSE.
-
-Author: Leonardo de Moura
-*/
-#include "kernel/kernel_exception.h"
-#include "library/kernel_bindings.h"
-#include "library/io_state.h"
-
-namespace lean {
-io_state::io_state():
-    m_formatter(mk_simple_formatter()),
-    m_regular_channel(std::make_shared<stdout_channel>()),
-    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
-}
-
-io_state::io_state(options const & opts, formatter const & fmt):
-    m_options(opts),
-    m_formatter(fmt),
-    m_regular_channel(std::make_shared<stdout_channel>()),
-    m_diagnostic_channel(std::make_shared<stderr_channel>()) {
-}
-
-io_state::~io_state() {}
-
-void io_state::set_regular_channel(std::shared_ptr<output_channel> const & out) {
-    if (out)
-        m_regular_channel = out;
-}
-
-void io_state::set_diagnostic_channel(std::shared_ptr<output_channel> const & out) {
-    if (out)
-        m_diagnostic_channel = out;
-}
-
-void io_state::set_options(options const & opts) {
-    m_options = opts;
-}
-
-void io_state::set_formatter(formatter const & f) {
-    m_formatter = f;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, endl_class) {
-    out.get_stream() << std::endl;
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, expr const & e) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(e, opts), opts);
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, object const & obj) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(obj, opts), opts);
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, environment const & env) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(out.get_formatter()(env, opts), opts);
-    return out;
-}
-
-io_state_stream const & operator<<(io_state_stream const & out, kernel_exception const & ex) {
-    options const & opts = out.get_options();
-    out.get_stream() << mk_pair(ex.pp(out.get_formatter(), opts), opts);
-    return out;
-}
-
-DECL_UDATA(io_state)
-
-int mk_io_state(lua_State * L) {
-    int nargs = lua_gettop(L);
-    if (nargs == 0)
-        return push_io_state(L, io_state());
-    else if (nargs == 1)
-        return push_io_state(L, io_state(to_io_state(L, 1)));
-    else
-        return push_io_state(L, io_state(to_options(L, 1), to_formatter(L, 2)));
-}
-
-int io_state_get_options(lua_State * L) {
-    return push_options(L, to_io_state(L, 1).get_options());
-}
-
-int io_state_get_formatter(lua_State * L) {
-    return push_formatter(L, to_io_state(L, 1).get_formatter());
-}
-
-int io_state_set_options(lua_State * L) {
-    to_io_state(L, 1).set_options(to_options(L, 2));
-    return 0;
-}
-
-static mutex g_print_mutex;
-
-static void print(io_state * ios, bool reg, char const * msg) {
-    if (ios) {
-        if (reg)
-            regular(*ios) << msg;
-        else
-            diagnostic(*ios) << msg;
-    } else {
-        std::cout << msg;
-    }
-}
-
-/** \brief Thread safe version of print function */
-static int print(lua_State * L, int start, bool reg) {
-    lock_guard<mutex> lock(g_print_mutex);
-    io_state * ios = get_io_state(L);
-    int n = lua_gettop(L);
-    int i;
-    lua_getglobal(L, "tostring");
-    for (i = start; i <= n; i++) {
-        char const * s;
-        size_t l;
-        lua_pushvalue(L, -1);
-        lua_pushvalue(L, i);
-        lua_call(L, 1, 1);
-        s = lua_tolstring(L, -1, &l);
-        if (s == NULL)
-            throw exception("'to_string' must return a string to 'print'");
-        if (i > start) {
-            print(ios, reg, "\t");
-        }
-        print(ios, reg, s);
-        lua_pop(L, 1);
-    }
-    print(ios, reg, "\n");
-    return 0;
-}
-
-static int print(lua_State * L, io_state & ios, int start, bool reg) {
-    set_io_state set(L, ios);
-    return print(L, start, reg);
-}
-
-static int print(lua_State * L) {
-    return print(L, 1, true);
-}
-
-int io_state_print_regular(lua_State * L) {
-    return print(L, to_io_state(L, 1), 2, true);
-}
-
-int io_state_print_diagnostic(lua_State * L) {
-    return print(L, to_io_state(L, 1), 2, false);
-}
-
-static const struct luaL_Reg io_state_m[] = {
-    {"__gc",             io_state_gc}, // never throws
-    {"get_options",      safe_function<io_state_get_options>},
-    {"set_options",      safe_function<io_state_set_options>},
-    {"get_formatter",    safe_function<io_state_get_formatter>},
-    {"print_diagnostic", safe_function<io_state_print_diagnostic>},
-    {"print_regular",    safe_function<io_state_print_regular>},
-    {"print",            safe_function<io_state_print_regular>},
-    {"diagnostic",       safe_function<io_state_print_diagnostic>},
-    {0, 0}
-};
-
-void open_io_state(lua_State * L) {
-    luaL_newmetatable(L, io_state_mt);
-    lua_pushvalue(L, -1);
-    lua_setfield(L, -2, "__index");
-    setfuncs(L, io_state_m, 0);
-
-    SET_GLOBAL_FUN(io_state_pred, "is_io_state");
-    SET_GLOBAL_FUN(mk_io_state, "io_state");
-    SET_GLOBAL_FUN(print, "print");
-}
-
-static char g_set_state_key;
-
-set_io_state::set_io_state(lua_State * L, io_state & st) {
-    m_state = L;
-    m_prev  = get_io_state(L);
-    lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
-    lua_pushlightuserdata(m_state, &st);
-    lua_settable(m_state, LUA_REGISTRYINDEX);
-    if (!m_prev)
-        m_prev_options = get_global_options(m_state);
-    set_global_options(m_state, st.get_options());
-}
-
-set_io_state::~set_io_state() {
-    lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
-    lua_pushlightuserdata(m_state, m_prev);
-    lua_settable(m_state, LUA_REGISTRYINDEX);
-    if (!m_prev)
-        set_global_options(m_state, m_prev_options);
-    else
-        set_global_options(m_state, m_prev->get_options());
-}
-
-io_state * get_io_state(lua_State * L) {
-    lua_pushlightuserdata(L, static_cast<void *>(&g_set_state_key));
-    lua_gettable(L, LUA_REGISTRYINDEX);
-    if (lua_islightuserdata(L, -1)) {
-        io_state * r = static_cast<io_state*>(lua_touserdata(L, -1));
-        if (r) {
-            lua_pop(L, 1);
-            options o = get_global_options(L);
-            r->set_options(o);
-            return r;
-        }
-    }
-    lua_pop(L, 1);
-    return nullptr;
-}
-}

src/library/kernel_bindings.cpp

@@ -18,10 +18,10 @@ Author: Leonardo de Moura
 #include "kernel/instantiate.h"
 #include "kernel/occurs.h"
 #include "kernel/builtin.h"
+#include "kernel/io_state.h"
 #include "kernel/type_checker.h"
 #include "library/expr_lt.h"
 #include "library/kernel_bindings.h"
-#include "library/io_state.h"
 
 // Lua Bindings for the Kernel classes. We do not include the Lua
 // bindings in the kernel because we do not want to inflate the Kernel.
@@ -1675,6 +1675,149 @@ void open_type_inferer(lua_State * L) {
     SET_GLOBAL_FUN(type_inferer_pred,        "is_type_inferer");
 }
 
+DECL_UDATA(io_state)
+
+int mk_io_state(lua_State * L) {
+    int nargs = lua_gettop(L);
+    if (nargs == 0)
+        return push_io_state(L, io_state());
+    else if (nargs == 1)
+        return push_io_state(L, io_state(to_io_state(L, 1)));
+    else
+        return push_io_state(L, io_state(to_options(L, 1), to_formatter(L, 2)));
+}
+
+int io_state_get_options(lua_State * L) {
+    return push_options(L, to_io_state(L, 1).get_options());
+}
+
+int io_state_get_formatter(lua_State * L) {
+    return push_formatter(L, to_io_state(L, 1).get_formatter());
+}
+
+int io_state_set_options(lua_State * L) {
+    to_io_state(L, 1).set_options(to_options(L, 2));
+    return 0;
+}
+
+static mutex g_print_mutex;
+
+static void print(io_state * ios, bool reg, char const * msg) {
+    if (ios) {
+        if (reg)
+            regular(*ios) << msg;
+        else
+            diagnostic(*ios) << msg;
+    } else {
+        std::cout << msg;
+    }
+}
+
+/** \brief Thread safe version of print function */
+static int print(lua_State * L, int start, bool reg) {
+    lock_guard<mutex> lock(g_print_mutex);
+    io_state * ios = get_io_state(L);
+    int n = lua_gettop(L);
+    int i;
+    lua_getglobal(L, "tostring");
+    for (i = start; i <= n; i++) {
+        char const * s;
+        size_t l;
+        lua_pushvalue(L, -1);
+        lua_pushvalue(L, i);
+        lua_call(L, 1, 1);
+        s = lua_tolstring(L, -1, &l);
+        if (s == NULL)
+            throw exception("'to_string' must return a string to 'print'");
+        if (i > start) {
+            print(ios, reg, "\t");
+        }
+        print(ios, reg, s);
+        lua_pop(L, 1);
+    }
+    print(ios, reg, "\n");
+    return 0;
+}
+
+static int print(lua_State * L, io_state & ios, int start, bool reg) {
+    set_io_state set(L, ios);
+    return print(L, start, reg);
+}
+
+static int print(lua_State * L) {
+    return print(L, 1, true);
+}
+
+int io_state_print_regular(lua_State * L) {
+    return print(L, to_io_state(L, 1), 2, true);
+}
+
+int io_state_print_diagnostic(lua_State * L) {
+    return print(L, to_io_state(L, 1), 2, false);
+}
+
+static const struct luaL_Reg io_state_m[] = {
+    {"__gc",             io_state_gc}, // never throws
+    {"get_options",      safe_function<io_state_get_options>},
+    {"set_options",      safe_function<io_state_set_options>},
+    {"get_formatter",    safe_function<io_state_get_formatter>},
+    {"print_diagnostic", safe_function<io_state_print_diagnostic>},
+    {"print_regular",    safe_function<io_state_print_regular>},
+    {"print",            safe_function<io_state_print_regular>},
+    {"diagnostic",       safe_function<io_state_print_diagnostic>},
+    {0, 0}
+};
+
+void open_io_state(lua_State * L) {
+    luaL_newmetatable(L, io_state_mt);
+    lua_pushvalue(L, -1);
+    lua_setfield(L, -2, "__index");
+    setfuncs(L, io_state_m, 0);
+
+    SET_GLOBAL_FUN(io_state_pred, "is_io_state");
+    SET_GLOBAL_FUN(mk_io_state, "io_state");
+    SET_GLOBAL_FUN(print, "print");
+}
+
+static char g_set_state_key;
+
+set_io_state::set_io_state(lua_State * L, io_state & st) {
+    m_state = L;
+    m_prev  = get_io_state(L);
+    lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
+    lua_pushlightuserdata(m_state, &st);
+    lua_settable(m_state, LUA_REGISTRYINDEX);
+    if (!m_prev)
+        m_prev_options = get_global_options(m_state);
+    set_global_options(m_state, st.get_options());
+}
+
+set_io_state::~set_io_state() {
+    lua_pushlightuserdata(m_state, static_cast<void *>(&g_set_state_key));
+    lua_pushlightuserdata(m_state, m_prev);
+    lua_settable(m_state, LUA_REGISTRYINDEX);
+    if (!m_prev)
+        set_global_options(m_state, m_prev_options);
+    else
+        set_global_options(m_state, m_prev->get_options());
+}
+
+io_state * get_io_state(lua_State * L) {
+    lua_pushlightuserdata(L, static_cast<void *>(&g_set_state_key));
+    lua_gettable(L, LUA_REGISTRYINDEX);
+    if (lua_islightuserdata(L, -1)) {
+        io_state * r = static_cast<io_state*>(lua_touserdata(L, -1));
+        if (r) {
+            lua_pop(L, 1);
+            options o = get_global_options(L);
+            r->set_options(o);
+            return r;
+        }
+    }
+    lua_pop(L, 1);
+    return nullptr;
+}
+
 void open_kernel_module(lua_State * L) {
     open_level(L);
     open_local_context(L);
@@ -1686,5 +1829,6 @@ void open_kernel_module(lua_State * L) {
     open_justification(L);
     open_metavar_env(L);
     open_type_inferer(L);
+    open_io_state(L);
 }
 }

src/library/kernel_bindings.h

@@ -21,6 +21,7 @@ UDATA_DEFS(object)
 UDATA_DEFS(environment)
 UDATA_DEFS(justification)
 UDATA_DEFS(metavar_env)
+UDATA_DEFS(io_state)
 int push_environment(lua_State * L, ro_environment const & env);
 int push_optional_expr(lua_State * L, optional<expr> const & e);
 int push_optional_justification(lua_State * L, optional<justification> const & j);
@@ -73,4 +74,22 @@ public:
     rw_shared_environment(lua_State * L, int idx);
     rw_shared_environment(lua_State * L);
 };
+/**
+   \brief Auxiliary class for temporarily setting the Lua registry of a Lua state
+   with a Lean io_state object.
+*/
+class set_io_state {
+    lua_State * m_state;
+    io_state *  m_prev;
+    options     m_prev_options;
+public:
+    set_io_state(lua_State * L, io_state & st);
+    ~set_io_state();
+};
+/**
+   \brief Return the Lean state object associated with the given Lua state.
+   Return nullptr is there is none.
+*/
+io_state * get_io_state(lua_State * L);
+void open_io_state(lua_State * L);
 }

src/library/register_module.h

@@ -7,7 +7,6 @@ Author: Leonardo de Moura
 #pragma once
 #include "util/script_state.h"
 #include "library/kernel_bindings.h"
-#include "library/io_state.h"
 #include "library/substitution.h"
 #include "library/fo_unify.h"
 #include "library/placeholder.h"
@@ -15,7 +14,6 @@ Author: Leonardo de Moura
 namespace lean {
 inline void open_core_module(lua_State * L) {
     open_kernel_module(L);
-    open_io_state(L);
     open_substitution(L);
     open_fo_unify(L);
     open_placeholder(L);

src/library/tactic/proof_state.h

@@ -12,7 +12,7 @@ Author: Leonardo de Moura
 #include "util/interrupt.h"
 #include "util/optional.h"
 #include "util/name_set.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/tactic/goal.h"
 #include "library/tactic/proof_builder.h"
 #include "library/tactic/cex_builder.h"

src/library/tactic/tactic.h

@@ -11,7 +11,7 @@ Author: Leonardo de Moura
 #include <string>
 #include "util/thread.h"
 #include "util/lazy_list.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/tactic/proof_state.h"
 
 namespace lean {

src/shell/lean.cpp

@@ -20,7 +20,7 @@ Author: Leonardo de Moura
 #include "kernel/environment.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/formatter.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/kernel_bindings.h"
 #include "frontends/lean/parser.h"
 #include "frontends/lean/frontend.h"

src/tests/kernel/metavar.cpp

@@ -19,8 +19,8 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/builtin.h"
+#include "kernel/io_state.h"
 #include "library/placeholder.h"
-#include "library/io_state.h"
 #include "library/arith/arith.h"
 #include "frontends/lean/frontend.h"
 using namespace lean;

src/tests/kernel/type_checker.cpp

@@ -20,9 +20,9 @@ Author: Leonardo de Moura
 #include "kernel/printer.h"
 #include "kernel/kernel_exception.h"
 #include "kernel/type_checker_justification.h"
+#include "kernel/io_state.h"
 #include "library/basic_thms.h"
 #include "library/arith/arith.h"
-#include "library/io_state.h"
 #include "frontends/lean/frontend.h"
 using namespace lean;
 

src/tests/library/rewriter/rewriter.cpp

@@ -10,7 +10,7 @@ Author: Soonho Kong
 #include "kernel/context.h"
 #include "kernel/expr.h"
 #include "kernel/printer.h"
-#include "library/io_state.h"
+#include "kernel/io_state.h"
 #include "library/all/all.h"
 #include "library/arith/arith.h"
 #include "library/arith/nat.h"