diff --git a/src/library/CMakeLists.txt b/src/library/CMakeLists.txt
index 6b2b95fd15..1b0720066d 100644
--- a/src/library/CMakeLists.txt
+++ b/src/library/CMakeLists.txt
@@ -17,7 +17,7 @@ add_library(library OBJECT deep_copy.cpp expr_lt.cpp io_state.cpp
   locals.cpp normalize.cpp discr_tree.cpp
   mt_task_queue.cpp st_task_queue.cpp
   library_task_builder.cpp
-  eval_helper.cpp
+  eval_helper.cpp io_env.cpp
   messages.cpp message_builder.cpp module_mgr.cpp comp_val.cpp
   documentation.cpp check.cpp arith_instance.cpp parray.cpp process.cpp
   pipe.cpp handle.cpp profiling.cpp time_task.cpp abstract_context_cache.cpp
diff --git a/src/library/init_module.cpp b/src/library/init_module.cpp
index 1fcab9d39e..9d85fd06a7 100644
--- a/src/library/init_module.cpp
+++ b/src/library/init_module.cpp
@@ -30,6 +30,7 @@ Author: Leonardo de Moura
 #include "library/fingerprint.h"
 #include "library/util.h"
 #include "library/pp_options.h"
+#include "library/io_env.h"
 #include "library/projection.h"
 #include "library/relation_manager.h"
 #include "library/user_recursors.h"
@@ -121,9 +122,11 @@ void initialize_library_module() {
     initialize_congr_lemma();
     initialize_parray();
     initialize_time_task();
+    initialize_io_env();
 }
 
 void finalize_library_module() {
+    finalize_io_env();
     finalize_time_task();
     finalize_parray();
     finalize_congr_lemma();
diff --git a/src/library/io_env.cpp b/src/library/io_env.cpp
new file mode 100644
index 0000000000..abcb089d55
--- /dev/null
+++ b/src/library/io_env.cpp
@@ -0,0 +1,51 @@
+/*
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Simon Hudon
+*/
+
+#include <string>
+#include "library/io_env.h"
+#include "util/path.h"
+
+namespace lean {
+struct io_env_ext : public environment_extension {
+    std::string m_cwd;
+    io_env_ext() : m_cwd(lgetcwd()) { }
+};
+
+struct io_env_ext_reg {
+    unsigned m_ext_id;
+    io_env_ext_reg() { m_ext_id = environment::register_extension(std::make_shared<io_env_ext>()); }
+};
+
+static io_env_ext_reg * g_ext = nullptr;
+static io_env_ext const & get_extension(environment const & env) {
+    return static_cast<io_env_ext const &>(env.get_extension(g_ext->m_ext_id));
+}
+
+static environment update(environment const & env, io_env_ext const & ext) {
+    return env.update(g_ext->m_ext_id, std::make_shared<io_env_ext>(ext));
+}
+
+environment set_cwd(environment const & env, std::string cwd) {
+    auto ext = get_extension(env);
+    ext.m_cwd = cwd;
+    return update(env, ext);
+}
+
+std::string get_cwd(environment const & env) {
+    auto & ext = get_extension(env);
+    return ext.m_cwd;
+}
+
+void initialize_io_env() {
+    g_ext     = new io_env_ext_reg();
+}
+
+void finalize_io_env() {
+    delete g_ext;
+}
+
+}
diff --git a/src/library/io_env.h b/src/library/io_env.h
new file mode 100644
index 0000000000..6eeb14e381
--- /dev/null
+++ b/src/library/io_env.h
@@ -0,0 +1,16 @@
+/*
+Copyright (c) 2019 Simon Hudon. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+
+Author: Simon Hudon
+*/
+
+#include <string>
+#include "kernel/environment.h"
+
+namespace lean {
+environment set_cwd(environment const & env, std::string cwd);
+std::string get_cwd(environment const & env);
+void initialize_io_env();
+void finalize_io_env();
+}
diff --git a/src/library/tactic/tactic_state.cpp b/src/library/tactic/tactic_state.cpp
index e9984d9fb4..ea8f4c616f 100644
--- a/src/library/tactic/tactic_state.cpp
+++ b/src/library/tactic/tactic_state.cpp
@@ -14,6 +14,7 @@ Author: Leonardo de Moura
 #include "library/pp_options.h"
 #include "library/trace.h"
 #include "library/util.h"
+#include "library/io_env.h"
 #include "library/cache_helper.h"
 #include "library/module.h"
 #include "library/check.h"
@@ -826,14 +827,17 @@ vm_obj tactic_add_aux_decl(vm_obj const & n, vm_obj const & type, vm_obj const &
     }
 }
 
-vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const & s) {
+vm_obj tactic_unsafe_run_io(vm_obj const &, vm_obj const & a, vm_obj const & _s) {
+    tactic_state s = tactic::to_state(_s);
+    auto env = s.env();
+    set_local_cwd(get_cwd(env));
     vm_obj r = invoke(a, mk_vm_unit());
     if (optional<vm_obj> a = is_io_result(r)) {
-        return tactic::mk_success(*a, tactic::to_state(s));
+        return tactic::mk_success(*a, set_env(s, set_cwd(env, get_local_cwd())));
     } else {
         optional<vm_obj> e = is_io_error(r);
         lean_assert(e);
-        return tactic::mk_exception(io_error_to_string(*e), tactic::to_state(s));
+        return tactic::mk_exception(io_error_to_string(*e), s);
     }
 }
 
diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index c9e015d6fd..a7f3171e93 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -59,6 +59,7 @@ Author: Leonardo de Moura
 #include <util/unit.h>
 #include "util/sstream.h"
 #include "util/utf8.h"
+#include "util/path.h"
 #include "library/handle.h"
 #include "library/io_state.h"
 #include "library/constants.h"
@@ -75,6 +76,25 @@ Author: Leonardo de Moura
 #include "library/kernel_serializer.h"
 
 namespace lean {
+
+MK_THREAD_LOCAL_GET(std::string, local_cwd, lgetcwd())
+
+std::string abspath(std::string const & path) {
+    return (sstream() << local_cwd() << "/" << path).str();
+}
+
+optional<std::string> local_realpath(std::string const & path) {
+    return try_realpath(abspath(path));
+}
+
+std::string const & get_local_cwd() {
+    return local_cwd();
+}
+
+void set_local_cwd(std::string const & cwd) {
+    local_cwd() = cwd;
+}
+
 vm_obj io_core(vm_obj const &, vm_obj const &) {
     return mk_vm_unit();
 }
@@ -186,13 +206,14 @@ char const * to_c_io_mode(unsigned int mode, bool is_bin) {
 }
 
 /* (mk_file_handle : string → io.mode → bool → m io.error handle) */
-static vm_obj fs_mk_file_handle(vm_obj const & fname, vm_obj const & m, vm_obj const & bin, vm_obj const &) {
+static vm_obj fs_mk_file_handle(vm_obj const & _fname, vm_obj const & m, vm_obj const & bin, vm_obj const &) {
     bool is_bin = to_bool(bin);
-    FILE * h = fopen(to_string(fname).c_str(), to_c_io_mode(cidx(m), is_bin));
+    auto fname = abspath(to_string(_fname));
+    FILE * h = fopen(fname.c_str(), to_c_io_mode(cidx(m), is_bin));
     if (h != nullptr)
         return mk_io_result(to_obj(std::make_shared<handle>(h, is_bin)));
     else
-        return mk_io_failure(sstream() << "failed to open file '" << to_string(fname) << "'");
+        return mk_io_failure(sstream() << "failed to open file '" << to_string(_fname) << "'");
 }
 
 static vm_obj mk_handle_has_been_closed_error() {
@@ -458,25 +479,30 @@ static int fs_stat(const char *path) {
     return FSTAT_MISC;
 }
 
-static vm_obj fs_file_exists(vm_obj const & path, vm_obj const &) {
-    bool ret = fs_stat(to_string(path).c_str()) == FSTAT_FILE;
+static vm_obj fs_file_exists(vm_obj const & _path, vm_obj const &) {
+    auto path = abspath(to_string(_path));
+    bool ret = fs_stat(path.c_str()) == FSTAT_FILE;
     return mk_io_result(mk_vm_bool(ret));
 }
 
-static vm_obj fs_dir_exists(vm_obj const & path, vm_obj const &) {
-    bool ret = fs_stat(to_string(path).c_str()) == FSTAT_DIR;
+static vm_obj fs_dir_exists(vm_obj const & _path, vm_obj const &) {
+    auto path = abspath(to_string(_path));
+    bool ret = fs_stat(path.c_str()) == FSTAT_DIR;
     return mk_io_result(mk_vm_bool(ret));
 }
 
-static vm_obj fs_remove(vm_obj const & path, vm_obj const &) {
-    if (std::remove(to_string(path).c_str()) != 0) {
+static vm_obj fs_remove(vm_obj const & _path, vm_obj const &) {
+    auto path = abspath(to_string(_path));
+    if (std::remove(path.c_str()) != 0) {
         return mk_io_failure(sstream() << "remove failed: " << strerror(errno));
     }
     return mk_io_result(mk_vm_unit());
 }
 
-static vm_obj fs_rename(vm_obj const & p1, vm_obj const & p2, vm_obj const &) {
-    if (std::rename(to_string(p1).c_str(), to_string(p2).c_str()) != 0) {
+static vm_obj fs_rename(vm_obj const & _p1, vm_obj const & _p2, vm_obj const &) {
+    auto p1 = abspath(to_string(_p1));
+    auto p2 = abspath(to_string(_p2));
+    if (std::rename(p1.c_str(), p2.c_str()) != 0) {
         return mk_io_failure(sstream() << "rename failed: " << strerror(errno));
     }
     return mk_io_result(mk_vm_unit());
@@ -531,18 +557,19 @@ int mkdir_recursive(const char *path) {
 }
 
 static vm_obj fs_mkdir(vm_obj const & _path, vm_obj const & rec, vm_obj const &) {
-    std::string path = to_string(_path);
+    auto path = abspath(to_string(_path));
     bool res = to_bool(rec) ? mkdir_recursive(path.c_str())
                             : mkdir_single(path.c_str());
     return mk_io_result(mk_vm_bool(!res));
 }
 
-static vm_obj fs_rmdir(vm_obj const & path, vm_obj const &) {
+static vm_obj fs_rmdir(vm_obj const & _path, vm_obj const &) {
     bool res;
+    auto path = abspath(to_string(_path));
 #if defined(__linux__) || defined(__APPLE__) || defined(LEAN_EMSCRIPTEN)
-    res = !rmdir(to_string(path).c_str());
+    res = !rmdir(path.c_str());
 #else
-    res = RemoveDirectoryA(to_string(path).c_str());
+    res = RemoveDirectoryA(path.c_str());
 #endif
     return mk_io_result(mk_vm_bool(res));
 }
@@ -664,9 +691,11 @@ static vm_obj io_process_spawn(vm_obj const & process_obj, vm_obj const &) {
     auto stdout_stdio = to_stdio(cfield(process_obj, 3));
     auto stderr_stdio = to_stdio(cfield(process_obj, 4));
 
-    optional<std::string> cwd;
+    std::string cwd;
     if (!is_none(cfield(process_obj, 5)))
         cwd = to_string(get_some_value(cfield(process_obj, 5)));
+    else
+        cwd = local_cwd();
 
     lean::process proc(cmd, stdin_stdio, stdout_stdio, stderr_stdio);
 
@@ -682,7 +711,7 @@ static vm_obj io_process_spawn(vm_obj const & process_obj, vm_obj const &) {
         return unit();
     });
 
-    if (cwd) proc.set_cwd(*cwd);
+    proc.set_cwd(cwd);
 
     return mk_io_result(to_obj(proc.spawn()));
 }
@@ -778,20 +807,15 @@ static vm_obj io_get_env(vm_obj const & k, vm_obj const &) {
 }
 
 static vm_obj io_get_cwd(vm_obj const &) {
-    char buffer[PATH_MAX];
-    auto cwd = getcwd(buffer, sizeof(buffer));
-    if (cwd) {
-        return mk_io_result(to_obj(std::string(cwd)));
-    } else {
-        return mk_io_failure("get_cwd failed");
-    }
+    return mk_io_result(to_obj(local_cwd()));
 }
 
-static vm_obj io_set_cwd(vm_obj const & cwd, vm_obj const &) {
-    if (chdir(to_string(cwd).c_str()) == 0) {
+static vm_obj io_set_cwd(vm_obj const & _path, vm_obj const &) {
+    if (auto path = local_realpath(to_string(_path))) {
+        local_cwd() = to_unix_path(*path);
         return mk_io_result(mk_vm_unit());
     } else {
-        return mk_io_failure("set_cwd failed");
+        return mk_io_failure(sstream() << "set_cwd failed");
     }
 }
 
diff --git a/src/library/vm/vm_io.h b/src/library/vm/vm_io.h
index a605e53945..9cfc94c6c7 100644
--- a/src/library/vm/vm_io.h
+++ b/src/library/vm/vm_io.h
@@ -24,6 +24,10 @@ std::string io_error_to_string(vm_obj const & o);
 
 void set_io_cmdline_args(std::vector<std::string> const & args);
 
+std::string const & get_local_cwd();
+
+void set_local_cwd(std::string const & cwd);
+
 void initialize_vm_io();
 void finalize_vm_io();
 }
diff --git a/src/util/path.cpp b/src/util/path.cpp
index 3457566970..1641f99cbd 100644
--- a/src/util/path.cpp
+++ b/src/util/path.cpp
@@ -13,6 +13,7 @@ Author: Leonardo de Moura, Gabriel Ebner
 #include <cstdlib>
 #include <fstream>
 #include <vector>
+#include <unistd.h>
 #include <sys/types.h>
 #include <sys/stat.h>
 #include "util/exception.h"
@@ -74,7 +75,6 @@ std::string get_exe_location() {
 bool is_path_sep(char c) { return c == g_path_sep; }
 #else
 // Linux version
-#include <unistd.h>
 #include <string.h>
 #include <limits.h> // NOLINT
 #include <stdio.h>
@@ -121,6 +121,14 @@ std::string normalize_path(std::string f) {
     return f;
 }
 
+std::string to_unix_path(std::string f) {
+    for (auto & c : f) {
+        if (c == '\\')
+            c = '/';
+    }
+    return f;
+}
+
 std::string get_path(std::string f) {
     while (true) {
         if (f.empty())
@@ -224,13 +232,13 @@ std::vector<std::string> read_dir(std::string const &dirname) {
     return files;
 }
 
-std::string lrealpath(std::string const & fname) {
+optional<std::string> try_realpath(std::string const & fname) {
 // return if in browser or WebWorker context
 #if defined(LEAN_EMSCRIPTEN)
     if (EM_ASM_INT({
         return (typeof window === 'object') || (typeof importScripts === 'function');
     })) {
-        return fname;
+        return optional<std::string>(fname);
     }
 #endif
 #if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN)
@@ -238,19 +246,36 @@ std::string lrealpath(std::string const & fname) {
     char buffer[BufferSize];
     DWORD retval = GetFullPathName(fname.c_str(), BufferSize, buffer, nullptr);
     if (retval == 0 || retval > BufferSize) {
-        return fname;
+        return optional<std::string>();
     } else {
-        return std::string(buffer);
+        return optional<std::string>(std::string(buffer));
     }
 #else
     char * tmp = realpath(fname.c_str(), nullptr);
     if (tmp) {
         std::string r(tmp);
         ::free(tmp);
-        return r;
+        return optional<std::string>(r);
     } else {
-        throw file_not_found_exception(fname);
+        return optional<std::string>();
     }
 #endif
 }
+
+std::string lrealpath(std::string const & fname) {
+    if (auto r = try_realpath(fname))
+        return *r;
+    else
+        throw file_not_found_exception(fname);
+}
+
+std::string lgetcwd() {
+    if (char * cd = getcwd(nullptr, 0)) {
+        std::string res(cd);
+        free(cd);
+        return res;
+    } else {
+        throw exception(strerror(errno));
+    }
+}
 }
diff --git a/src/util/path.h b/src/util/path.h
index 53f28b4cc2..ce041c931f 100644
--- a/src/util/path.h
+++ b/src/util/path.h
@@ -28,6 +28,8 @@ bool is_path_sep(char c);
 
 std::string normalize_path(std::string f);
 
+std::string to_unix_path(std::string f);
+
 /** \brief Find all files with the given extension recursively. */
 void find_files(std::string const & base, char const * ext, std::vector<std::string> & files);
 bool has_file_ext(std::string const & fname, char const * ext);
@@ -44,4 +46,7 @@ std::vector<std::string> read_dir(std::string const & dirname);
 time_t get_mtime(std::string const & fname);
 
 std::string lrealpath(std::string const & fname);
+optional<std::string> try_realpath(std::string const & fname);
+
+std::string lgetcwd();
 }
diff --git a/tests/lean/set_cwd.lean b/tests/lean/set_cwd.lean
new file mode 100644
index 0000000000..8d141f2b49
--- /dev/null
+++ b/tests/lean/set_cwd.lean
@@ -0,0 +1,33 @@
+import system.io
+
+def this_dir := "tests/lean"
+
+meta def lean_root : tactic string :=
+tactic.unsafe_run_io $ do
+  dir ← io.env.get_cwd,
+  return $ list.as_string $ dir.to_list.take (dir.length - this_dir.length - 1)
+
+open tactic
+
+meta def mk_def {α} [reflected α] [has_reflect α] (n : name) (tac : tactic α) : tactic unit :=
+do let t := `(α),
+   v ← tac,
+   add_decl $ mk_definition n [] t (reflect v)
+
+run_cmd mk_def `root_dir lean_root
+
+meta def test' : tactic unit := (tactic.unsafe_run_io
+(do io.env.set_cwd "lean",
+    io.env.get_cwd >>= io.put_str_ln) >> failed)
+
+run_cmd test' <|> trace "foo"
+
+def strip_prefix (p s : string) : string :=
+list.as_string $ s.to_list.drop p.length
+
+meta def test : tactic unit := tactic.unsafe_run_io $
+do io.env.get_cwd >>= io.put_str_ln ∘ strip_prefix root_dir,
+   io.env.set_cwd "..",
+   io.env.get_cwd >>= io.put_str_ln ∘ strip_prefix root_dir
+
+run_cmd (test >> test >> tactic.failed) <|> test
diff --git a/tests/lean/set_cwd.lean.expected.out b/tests/lean/set_cwd.lean.expected.out
new file mode 100644
index 0000000000..9deafaede5
--- /dev/null
+++ b/tests/lean/set_cwd.lean.expected.out
@@ -0,0 +1,7 @@
+foo
+/tests/lean
+/tests
+/tests
+
+/tests/lean
+/tests