diff --git a/leanpkg/leanpkg/main.lean b/leanpkg/leanpkg/main.lean
index 5b45b8d014..5d9840e376 100644
--- a/leanpkg/leanpkg/main.lean
+++ b/leanpkg/leanpkg/main.lean
@@ -20,8 +20,9 @@ def write_manifest (d : manifest) (fn := leanpkg_toml_fn) : io unit :=
 write_file fn (to_string d)
 
 -- TODO(gabriel): implement a cross-platform api
-def get_dot_lean_dir : io string :=
-io.cmd "bash" ["-c", "echo -n ~/.lean"]
+def get_dot_lean_dir : io string := do
+some home ← io.env.get "HOME" | io.fail "environment variable HOME is not set",
+return $ home ++ "/.lean"
 
 -- TODO(gabriel): file existence testing
 def exists_file (f : string) : io bool := do
diff --git a/library/system/io.lean b/library/system/io.lean
index ac1d90f023..f2aed01582 100644
--- a/library/system/io.lean
+++ b/library/system/io.lean
@@ -30,6 +30,10 @@ structure io.file_system (handle : Type) (m : Type → Type → Type) :=
 (stdout         : m io.error handle)
 (stderr         : m io.error handle)
 
+structure io.environment (m : Type → Type → Type) :=
+(get_env : string → m io.error (option string))
+-- we don't provide set_env as it is (thread-)unsafe (at least with glibc)
+
 inductive io.process.stdio
 | piped
 | inherit
@@ -66,6 +70,7 @@ class io.interface :=
 (term     : io.terminal m)
 (fs       : io.file_system handle m)
 (process  : io.process handle m)
+(env      : io.environment m)
 
 variable [io.interface]
 
@@ -133,6 +138,13 @@ interface.fs.stderr
 def stdout : io handle :=
 interface.fs.stdout
 
+namespace env
+
+def get (env_var : string) : io (option string) :=
+interface.env.get_env env_var
+
+end env
+
 namespace fs
 def is_eof : handle → io bool :=
 interface.fs.is_eof
diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp
index 75d19382c2..27be71b2a6 100644
--- a/src/library/vm/vm_io.cpp
+++ b/src/library/vm/vm_io.cpp
@@ -425,6 +425,19 @@ static vm_obj io_iterate(vm_obj const &, vm_obj const &, vm_obj const & a, vm_ob
     }
 }
 
+static vm_obj mk_io_env() {
+    return mk_vm_constructor(0, {
+        // get_env
+        mk_native_closure([] (vm_obj const & k, vm_obj const &) {
+            if (auto v = getenv(to_string(k).c_str())) {
+                return mk_io_result(mk_vm_some(to_obj(std::string(v))));
+            } else {
+                return mk_io_result(mk_vm_none());
+            }
+        }),
+    });
+}
+
 /*
 class io.interface :=
 (m        : Type → Type → Type)
@@ -438,10 +451,10 @@ class io.interface :=
 (term     : io.terminal m)
 (fs       : io.file_system handle m)
 (process  : io.process io.error handle m)
+(env      : io.environment _)
 */
 vm_obj mk_io_interface(std::vector<std::string> const & cmdline_args) {
-    constexpr size_t num_fields = 7;
-    vm_obj fields[num_fields] = {
+    return mk_vm_constructor(0, {
         mk_native_closure(io_monad),
         mk_native_closure(io_catch),
         mk_native_closure(io_fail),
@@ -449,8 +462,8 @@ vm_obj mk_io_interface(std::vector<std::string> const & cmdline_args) {
         mk_terminal(cmdline_args),
         mk_fs(),
         mk_process(),
-    };
-    return mk_vm_constructor(0, num_fields, fields);
+        mk_io_env(),
+    });
 }
 
 vm_obj mk_io_interface() {