From 2a120553de35b11104329b7b9933ed127f8d25a1 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon.hudon@gmail.com>
Date: Thu, 16 May 2019 16:35:49 -0400
Subject: [PATCH 1/4] WIP: cwd in environment objects

---
 src/library/CMakeLists.txt           |   2 +-
 src/library/init_module.cpp          |   3 +
 src/library/io_env.cpp               |  44 +++++++++++
 src/library/io_env.h                 |   9 +++
 src/library/tactic/tactic_state.cpp  |  10 ++-
 src/library/vm/vm_io.cpp             | 114 ++++++++++++++++++---------
 src/library/vm/vm_io.h               |   4 +
 src/util/path.cpp                    |  11 +++
 src/util/path.h                      |   2 +
 tests/lean/set_cwd.lean              |  33 ++++++++
 tests/lean/set_cwd.lean.expected.out |   7 ++
 11 files changed, 199 insertions(+), 40 deletions(-)
 create mode 100644 src/library/io_env.cpp
 create mode 100644 src/library/io_env.h
 create mode 100644 tests/lean/set_cwd.lean
 create mode 100644 tests/lean/set_cwd.lean.expected.out

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..4f9306aaf7
--- /dev/null
+++ b/src/library/io_env.cpp
@@ -0,0 +1,44 @@
+
+#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..a0e24a61c9
--- /dev/null
+++ b/src/library/io_env.h
@@ -0,0 +1,9 @@
+
+#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..b108db6ae5 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,21 @@ Author: Leonardo de Moura
 #include "library/kernel_serializer.h"
 
 namespace lean {
+
+MK_THREAD_LOCAL_GET(std::string, local_cwd, lgetcwd())
+
+std::string local_realpath(std::string const & path) {
+    return lrealpath(local_cwd() + "/" + 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();
 }
@@ -187,12 +203,16 @@ 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 &) {
-    bool is_bin = to_bool(bin);
-    FILE * h = fopen(to_string(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) << "'");
+    try {
+        bool is_bin = to_bool(bin);
+        FILE * h = fopen(local_realpath(to_string(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) << "'");
+    } catch (throwable & e) {
+        return mk_io_failure(sstream() << "mk_file_handle failed: " << e.what());
+    }
 }
 
 static vm_obj mk_handle_has_been_closed_error() {
@@ -459,27 +479,44 @@ static int fs_stat(const char *path) {
 }
 
 static vm_obj fs_file_exists(vm_obj const & path, vm_obj const &) {
-    bool ret = fs_stat(to_string(path).c_str()) == FSTAT_FILE;
-    return mk_io_result(mk_vm_bool(ret));
+    try {
+        bool ret = fs_stat(local_realpath(to_string(path)).c_str()) == FSTAT_FILE;
+        return mk_io_result(mk_vm_bool(ret));
+    } catch (throwable & e) {
+        return mk_io_result(mk_vm_bool(false));
+    }
 }
 
 static vm_obj fs_dir_exists(vm_obj const & path, vm_obj const &) {
-    bool ret = fs_stat(to_string(path).c_str()) == FSTAT_DIR;
-    return mk_io_result(mk_vm_bool(ret));
+    try {
+        bool ret = fs_stat(local_realpath(to_string(path)).c_str()) == FSTAT_DIR;
+        return mk_io_result(mk_vm_bool(ret));
+    } catch (throwable & e) {
+        return mk_io_result(mk_vm_bool(false));
+    }
 }
 
 static vm_obj fs_remove(vm_obj const & path, vm_obj const &) {
-    if (std::remove(to_string(path).c_str()) != 0) {
-        return mk_io_failure(sstream() << "remove failed: " << strerror(errno));
+    try {
+        if (std::remove(local_realpath(to_string(path)).c_str()) != 0) {
+            return mk_io_failure(sstream() << "remove failed: " << strerror(errno));
+        }
+        return mk_io_result(mk_vm_unit());
+    } catch (throwable & e) {
+        return mk_io_failure(sstream() << "remove failed: " << e.what());
     }
-    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) {
-        return mk_io_failure(sstream() << "rename failed: " << strerror(errno));
+    try {
+        if (std::rename(local_realpath(to_string(p1)).c_str(),
+                        local_realpath(to_string(p2)).c_str()) != 0) {
+            return mk_io_failure(sstream() << "rename failed: " << strerror(errno));
+        }
+        return mk_io_result(mk_vm_unit());
+    } catch (throwable & e) {
+        return mk_io_failure(sstream() << "rename failed: " << e.what());
     }
-    return mk_io_result(mk_vm_unit());
 }
 
 int mkdir_single(const char *path) {
@@ -531,20 +568,28 @@ 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);
-    bool res = to_bool(rec) ? mkdir_recursive(path.c_str())
-                            : mkdir_single(path.c_str());
-    return mk_io_result(mk_vm_bool(!res));
+    try {
+        std::string path = local_realpath(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));
+    } catch (throwable & e) {
+        return mk_io_failure(sstream() << "mkdir failed: " << e.what());
+    }
 }
 
 static vm_obj fs_rmdir(vm_obj const & path, vm_obj const &) {
-    bool res;
+    try {
+        bool res;
 #if defined(__linux__) || defined(__APPLE__) || defined(LEAN_EMSCRIPTEN)
-    res = !rmdir(to_string(path).c_str());
+        res = !rmdir(local_realpath(to_string(path)).c_str());
 #else
-    res = RemoveDirectoryA(to_string(path).c_str());
+        res = RemoveDirectoryA(local_realpath(to_string(path)).c_str());
 #endif
-    return mk_io_result(mk_vm_bool(res));
+        return mk_io_result(mk_vm_bool(res));
+    } catch (throwable & e) {
+        return mk_io_failure(sstream() << "rmdir failed: " << e.what());
+    }
 }
 
 /*
@@ -664,9 +709,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 +729,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 +825,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) {
+    try {
+        local_cwd() = local_realpath(to_string(cwd));
         return mk_io_result(mk_vm_unit());
-    } else {
-        return mk_io_failure("set_cwd failed");
+    } catch (throwable & e) {
+        return mk_io_failure(sstream() << "set_cwd failed: " << e.what());
     }
 }
 
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..1c2c022800 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"
@@ -253,4 +254,14 @@ std::string lrealpath(std::string const & fname) {
     }
 #endif
 }
+
+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..0e70ae031e 100644
--- a/src/util/path.h
+++ b/src/util/path.h
@@ -44,4 +44,6 @@ 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);
+
+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

From d58b050b00d87d49ee87b6c21dd23b1f14461ad0 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon.hudon@gmail.com>
Date: Fri, 17 May 2019 19:50:03 -0400
Subject: [PATCH 2/4] fix absolute paths to non-existant files

---
 src/library/io_env.cpp   |   7 +++
 src/library/io_env.h     |   7 +++
 src/library/vm/vm_io.cpp | 114 +++++++++++++++++----------------------
 src/util/path.cpp        |  20 ++++---
 src/util/path.h          |   1 +
 5 files changed, 76 insertions(+), 73 deletions(-)

diff --git a/src/library/io_env.cpp b/src/library/io_env.cpp
index 4f9306aaf7..abcb089d55 100644
--- a/src/library/io_env.cpp
+++ b/src/library/io_env.cpp
@@ -1,4 +1,11 @@
+/*
+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"
 
diff --git a/src/library/io_env.h b/src/library/io_env.h
index a0e24a61c9..6eeb14e381 100644
--- a/src/library/io_env.h
+++ b/src/library/io_env.h
@@ -1,4 +1,11 @@
+/*
+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 {
diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index b108db6ae5..ed14d32d9f 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -79,8 +79,12 @@ namespace lean {
 
 MK_THREAD_LOCAL_GET(std::string, local_cwd, lgetcwd())
 
-std::string local_realpath(std::string const & path) {
-    return lrealpath(local_cwd() + "/" + path);
+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() {
@@ -202,17 +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 &) {
-    try {
-        bool is_bin = to_bool(bin);
-        FILE * h = fopen(local_realpath(to_string(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) << "'");
-    } catch (throwable & e) {
-        return mk_io_failure(sstream() << "mk_file_handle failed: " << e.what());
-    }
+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);
+    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) << "'");
 }
 
 static vm_obj mk_handle_has_been_closed_error() {
@@ -478,45 +479,33 @@ static int fs_stat(const char *path) {
     return FSTAT_MISC;
 }
 
-static vm_obj fs_file_exists(vm_obj const & path, vm_obj const &) {
-    try {
-        bool ret = fs_stat(local_realpath(to_string(path)).c_str()) == FSTAT_FILE;
-        return mk_io_result(mk_vm_bool(ret));
-    } catch (throwable & e) {
-        return mk_io_result(mk_vm_bool(false));
-    }
+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 &) {
-    try {
-        bool ret = fs_stat(local_realpath(to_string(path)).c_str()) == FSTAT_DIR;
-        return mk_io_result(mk_vm_bool(ret));
-    } catch (throwable & e) {
-        return mk_io_result(mk_vm_bool(false));
-    }
+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 &) {
-    try {
-        if (std::remove(local_realpath(to_string(path)).c_str()) != 0) {
-            return mk_io_failure(sstream() << "remove failed: " << strerror(errno));
-        }
-        return mk_io_result(mk_vm_unit());
-    } catch (throwable & e) {
-        return mk_io_failure(sstream() << "remove failed: " << e.what());
+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 &) {
-    try {
-        if (std::rename(local_realpath(to_string(p1)).c_str(),
-                        local_realpath(to_string(p2)).c_str()) != 0) {
-            return mk_io_failure(sstream() << "rename failed: " << strerror(errno));
-        }
-        return mk_io_result(mk_vm_unit());
-    } catch (throwable & e) {
-        return mk_io_failure(sstream() << "rename failed: " << e.what());
+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());
 }
 
 int mkdir_single(const char *path) {
@@ -568,28 +557,21 @@ int mkdir_recursive(const char *path) {
 }
 
 static vm_obj fs_mkdir(vm_obj const & _path, vm_obj const & rec, vm_obj const &) {
-    try {
-        std::string path = local_realpath(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));
-    } catch (throwable & e) {
-        return mk_io_failure(sstream() << "mkdir failed: " << e.what());
-    }
+    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 &) {
-    try {
-        bool res;
+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(local_realpath(to_string(path)).c_str());
+    res = !rmdir(path.c_str());
 #else
-        res = RemoveDirectoryA(local_realpath(to_string(path)).c_str());
+    res = RemoveDirectoryA(path.c_str());
 #endif
-        return mk_io_result(mk_vm_bool(res));
-    } catch (throwable & e) {
-        return mk_io_failure(sstream() << "rmdir failed: " << e.what());
-    }
+    return mk_io_result(mk_vm_bool(res));
 }
 
 /*
@@ -828,12 +810,12 @@ static vm_obj io_get_cwd(vm_obj const &) {
     return mk_io_result(to_obj(local_cwd()));
 }
 
-static vm_obj io_set_cwd(vm_obj const & cwd, vm_obj const &) {
-    try {
-        local_cwd() = local_realpath(to_string(cwd));
+static vm_obj io_set_cwd(vm_obj const & _path, vm_obj const &) {
+    if (auto path = local_realpath(to_string(_path))) {
+        local_cwd() = *path;
         return mk_io_result(mk_vm_unit());
-    } catch (throwable & e) {
-        return mk_io_failure(sstream() << "set_cwd failed: " << e.what());
+    } else {
+        return mk_io_failure(sstream() << "set_cwd failed");
     }
 }
 
diff --git a/src/util/path.cpp b/src/util/path.cpp
index 1c2c022800..9816ed5869 100644
--- a/src/util/path.cpp
+++ b/src/util/path.cpp
@@ -75,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>
@@ -225,13 +224,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)
@@ -239,22 +238,29 @@ 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);
diff --git a/src/util/path.h b/src/util/path.h
index 0e70ae031e..c66f6a50d8 100644
--- a/src/util/path.h
+++ b/src/util/path.h
@@ -44,6 +44,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();
 }

From ae55905cd82dce1306ee7b911066460be4d7cb3d Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon.hudon@gmail.com>
Date: Sat, 18 May 2019 21:13:34 -0400
Subject: [PATCH 3/4] fix OS-dependent path separators

---
 src/library/vm/vm_io.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index ed14d32d9f..4099e8f870 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -80,7 +80,7 @@ namespace lean {
 MK_THREAD_LOCAL_GET(std::string, local_cwd, lgetcwd())
 
 std::string abspath(std::string const & path) {
-    return (sstream() << local_cwd() << "/" << path).str();
+    return normalize_path( (sstream() << local_cwd() << "/" << path).str() );
 }
 
 optional<std::string> local_realpath(std::string const & path) {

From 9dafd212a9f5387728c85cafb6836483fe767f97 Mon Sep 17 00:00:00 2001
From: Simon Hudon <simon.hudon@gmail.com>
Date: Sun, 19 May 2019 01:28:56 -0400
Subject: [PATCH 4/4] use unix path format in `io` primitives

---
 src/library/vm/vm_io.cpp | 4 ++--
 src/util/path.cpp        | 8 ++++++++
 src/util/path.h          | 2 ++
 3 files changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index 4099e8f870..a7f3171e93 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -80,7 +80,7 @@ namespace lean {
 MK_THREAD_LOCAL_GET(std::string, local_cwd, lgetcwd())
 
 std::string abspath(std::string const & path) {
-    return normalize_path( (sstream() << local_cwd() << "/" << path).str() );
+    return (sstream() << local_cwd() << "/" << path).str();
 }
 
 optional<std::string> local_realpath(std::string const & path) {
@@ -812,7 +812,7 @@ static vm_obj io_get_cwd(vm_obj const &) {
 
 static vm_obj io_set_cwd(vm_obj const & _path, vm_obj const &) {
     if (auto path = local_realpath(to_string(_path))) {
-        local_cwd() = *path;
+        local_cwd() = to_unix_path(*path);
         return mk_io_result(mk_vm_unit());
     } else {
         return mk_io_failure(sstream() << "set_cwd failed");
diff --git a/src/util/path.cpp b/src/util/path.cpp
index 9816ed5869..1641f99cbd 100644
--- a/src/util/path.cpp
+++ b/src/util/path.cpp
@@ -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())
diff --git a/src/util/path.h b/src/util/path.h
index c66f6a50d8..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);