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

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

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

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"
@@ -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,33 +232,50 @@ 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)
     constexpr unsigned BufferSize = 8192;
     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));
+    }
+}
 }