WIP: cwd in environment objects

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

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();

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;
+}
+
+}

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();
+}

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);
     }
 }
 

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());
     }
 }
 

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();
 }

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));
+    }
+}
 }

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();
 }

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

tests/lean/set_cwd.lean.expected.out

@@ -0,0 +1,7 @@
+foo
+/tests/lean
+/tests
+/tests
+
+/tests/lean
+/tests