diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean
index b0ba5ee94823..1753e5a4b99d 100644
--- a/src/Init/System/IO.lean
+++ b/src/Init/System/IO.lean
@@ -153,15 +153,17 @@ structure FS.Stream where
   getLine : IO String
   putStr  : String → IO Unit
 
-namespace Prim
 open FS
 
 @[extern "lean_get_stdin"] constant getStdin  : IO FS.Stream
 @[extern "lean_get_stdout"] constant getStdout : IO FS.Stream
 @[extern "lean_get_stderr"] constant getStderr : IO FS.Stream
 
+/-- Replaces the stdin stream of the current thread and returns its previous value. -/
 @[extern "lean_get_set_stdin"] constant setStdin  : FS.Stream → IO FS.Stream
+/-- Replaces the stdout stream of the current thread and returns its previous value. -/
 @[extern "lean_get_set_stdout"] constant setStdout : FS.Stream → IO FS.Stream
+/-- Replaces the stderr stream of the current thread and returns its previous value. -/
 @[extern "lean_get_set_stderr"] constant setStderr : FS.Stream → IO FS.Stream
 
 @[specialize] partial def iterate (a : α) (f : α → IO (Sum α β)) : IO β := do
@@ -170,8 +172,11 @@ open FS
   | Sum.inl a => iterate a f
   | Sum.inr b => pure b
 
--- @[export lean_fopen_flags]
-def fopenFlags (m : FS.Mode) (b : Bool) : String :=
+namespace FS
+
+namespace Handle
+
+private def fopenFlags (m : FS.Mode) (b : Bool) : String :=
   let mode :=
     match m with
     | FS.Mode.read      => "r"
@@ -181,74 +186,72 @@ def fopenFlags (m : FS.Mode) (b : Bool) : String :=
   let bin := if b then "b" else "t"
   mode ++ bin
 
-@[extern "lean_io_prim_handle_mk"] constant Handle.mk (fn : @& FilePath) (mode : @& String) : IO Handle
-@[extern "lean_io_prim_handle_is_eof"] constant Handle.isEof (h : @& Handle) : IO Bool
-@[extern "lean_io_prim_handle_flush"] constant Handle.flush (h : @& Handle) : IO Unit
-@[extern "lean_io_prim_handle_read"] constant Handle.read  (h : @& Handle) (bytes : USize) : IO ByteArray
-@[extern "lean_io_prim_handle_write"] constant Handle.write (h : @& Handle) (buffer : @& ByteArray) : IO Unit
+@[extern "lean_io_prim_handle_mk"] constant mkPrim (fn : @& FilePath) (mode : @& String) : IO Handle
 
-@[extern "lean_io_prim_handle_get_line"] constant Handle.getLine (h : @& Handle) : IO String
-@[extern "lean_io_prim_handle_put_str"] constant Handle.putStr (h : @& Handle) (s : @& String) : IO Unit
+def mk (fn : FilePath) (Mode : Mode) (bin : Bool := true) : IO Handle :=
+  mkPrim fn (fopenFlags Mode bin)
+
+/--
+Returns whether the end of the file has been reached while reading a file.
+`h.isEof` returns true /after/ the first attempt at reading past the end of `h`.
+Once `h.isEof` is true, reading `h` will always return an empty array.
+-/
+@[extern "lean_io_prim_handle_is_eof"] constant isEof (h : @& Handle) : IO Bool
+@[extern "lean_io_prim_handle_flush"] constant flush (h : @& Handle) : IO Unit
+@[extern "lean_io_prim_handle_read"] constant read  (h : @& Handle) (bytes : USize) : IO ByteArray
+@[extern "lean_io_prim_handle_write"] constant write (h : @& Handle) (buffer : @& ByteArray) : IO Unit
+
+@[extern "lean_io_prim_handle_get_line"] constant getLine (h : @& Handle) : IO String
+@[extern "lean_io_prim_handle_put_str"] constant putStr (h : @& Handle) (s : @& String) : IO Unit
+
+end Handle
 
-@[extern "lean_io_getenv"] constant getEnv (var : @& String) : IO (Option String)
 @[extern "lean_io_realpath"] constant realPath (fname : FilePath) : IO FilePath
 @[extern "lean_io_remove_file"] constant removeFile (fname : @& FilePath) : IO Unit
+@[extern "lean_io_create_dir"] constant createDir : @& FilePath → IO Unit
+
+end FS
+
+@[extern "lean_io_getenv"] constant getEnv (var : @& String) : IO (Option String)
 @[extern "lean_io_app_path"] constant appPath : IO FilePath
 @[extern "lean_io_current_dir"] constant currentDir : IO FilePath
 
-end Prim
-
 namespace FS
-variable [Monad m] [MonadLiftT IO m]
-
-def Handle.mk (fn : FilePath) (Mode : Mode) (bin : Bool := true) : m Handle :=
-  liftM (Prim.Handle.mk fn (Prim.fopenFlags Mode bin))
 
 @[inline]
-def withFile (fn : FilePath) (mode : Mode) (f : Handle → m α) : m α :=
+def withFile (fn : FilePath) (mode : Mode) (f : Handle → IO α) : IO α :=
   Handle.mk fn mode >>= f
 
-/-- returns whether the end of the file has been reached while reading a file.
-`h.isEof` returns true /after/ the first attempt at reading past the end of `h`.
-Once `h.isEof` is true, the reading `h` raises `IO.Error.eof`.
--/
-def Handle.isEof : Handle → m Bool := liftM ∘ Prim.Handle.isEof
-def Handle.flush : Handle → m Unit := liftM ∘ Prim.Handle.flush
-def Handle.read (h : Handle) (bytes : Nat) : m ByteArray := liftM (Prim.Handle.read h (USize.ofNat bytes))
-def Handle.write (h : Handle) (s : ByteArray) : m Unit := liftM (Prim.Handle.write h s)
-
-def Handle.getLine : Handle → m String := liftM ∘ Prim.Handle.getLine
-
-def Handle.putStr (h : Handle) (s : String) : m Unit :=
-  liftM <| Prim.Handle.putStr h s
-
-def Handle.putStrLn (h : Handle) (s : String) : m Unit :=
+def Handle.putStrLn (h : Handle) (s : String) : IO Unit :=
   h.putStr (s.push '\n')
 
-partial def Handle.readBinToEnd (h : Handle) : m ByteArray := do
-  let rec loop (acc : ByteArray) : m ByteArray := do
-    if ← h.isEof then
+partial def Handle.readBinToEnd (h : Handle) : IO ByteArray := do
+  let rec loop (acc : ByteArray) : IO ByteArray := do
+    let buf ← h.read 1024
+    if buf.isEmpty then
       return acc
     else
-      let buf ← h.read 1024
       loop (acc ++ buf)
   loop ByteArray.empty
 
-partial def Handle.readToEnd (h : Handle) : m String := do
-  let rec read (s : String) := do
+partial def Handle.readToEnd (h : Handle) : IO String := do
+  let rec loop (s : String) := do
     let line ← h.getLine
-    if line.length == 0 then pure s else read (s ++ line)
-  read ""
+    if line.isEmpty then
+      return s
+    else
+      loop (s ++ line)
+  loop ""
 
-def readBinFile (fname : FilePath) : m ByteArray := do
+def readBinFile (fname : FilePath) : IO ByteArray := do
   let h ← Handle.mk fname Mode.read true
   h.readBinToEnd
 
-def readFile (fname : FilePath) : m String := do
+def readFile (fname : FilePath) : IO String := do
   let h ← Handle.mk fname Mode.read false
   h.readToEnd
 
-partial def lines (fname : FilePath) : m (Array String) := do
+partial def lines (fname : FilePath) : IO (Array String) := do
   let h ← Handle.mk fname Mode.read false
   let rec read (lines : Array String) := do
     let line ← h.getLine
@@ -262,16 +265,16 @@ partial def lines (fname : FilePath) : m (Array String) := do
       pure <| lines.push line
   read #[]
 
-def writeBinFile (fname : FilePath) (content : ByteArray) : m Unit := do
+def writeBinFile (fname : FilePath) (content : ByteArray) : IO Unit := do
   let h ← Handle.mk fname Mode.write true
   h.write content
 
-def writeFile (fname : FilePath) (content : String) : m Unit := do
+def writeFile (fname : FilePath) (content : String) : IO Unit := do
   let h ← Handle.mk fname Mode.write false
   h.putStr content
 
-def Stream.putStrLn (strm : FS.Stream) (s : String) : m Unit :=
-  liftM (strm.putStr (s.push '\n'))
+def Stream.putStrLn (strm : FS.Stream) (s : String) : IO Unit :=
+  strm.putStr (s.push '\n')
 
 structure DirEntry where
   root     : FilePath
@@ -309,7 +312,6 @@ end IO
 
 namespace System.FilePath
 open IO
-variable [Monad m] [MonadLiftT IO m]
 
 @[extern "lean_io_read_dir"]
 constant readDir : @& FilePath → IO (Array IO.FS.DirEntry)
@@ -329,34 +331,19 @@ def pathExists (p : FilePath) : IO Bool :=
 end System.FilePath
 
 namespace IO
-section
-variable [Monad m] [MonadLiftT IO m]
-
-def getStdin : m FS.Stream := liftM Prim.getStdin
-def getStdout : m FS.Stream := liftM Prim.getStdout
-def getStderr : m FS.Stream := liftM Prim.getStderr
-
-/-- Replaces the stdin stream of the current thread and returns its previous value. -/
-def setStdin : FS.Stream → m FS.Stream := liftM ∘ Prim.setStdin
-
-/-- Replaces the stdout stream of the current thread and returns its previous value. -/
-def setStdout : FS.Stream → m FS.Stream := liftM ∘ Prim.setStdout
-
-/-- Replaces the stderr stream of the current thread and returns its previous value. -/
-def setStderr : FS.Stream → m FS.Stream := liftM ∘ Prim.setStderr
 
-def withStdin [MonadFinally m] (h : FS.Stream) (x : m α) : m α := do
+def withStdin [Monad m] [MonadFinally m] [MonadLiftT IO m] (h : FS.Stream) (x : m α) : m α := do
   let prev ← setStdin h
   try x finally discard <| setStdin prev
 
-def withStdout [MonadFinally m] (h : FS.Stream) (x : m α) : m α := do
+def withStdout [Monad m] [MonadFinally m] [MonadLiftT IO m] (h : FS.Stream) (x : m α) : m α := do
   let prev ← setStdout h
   try
     x
   finally
     discard <| setStdout prev
 
-def withStderr [MonadFinally m] (h : FS.Stream) (x : m α) : m α := do
+def withStderr [Monad m] [MonadFinally m] [MonadLiftT IO m] (h : FS.Stream) (x : m α) : m α := do
   let prev ← setStderr h
   try x finally discard <| setStderr prev
 
@@ -369,7 +356,7 @@ def println [ToString α] (s : α) : IO Unit :=
 
 def eprint [ToString α] (s : α) : IO Unit := do
   let out ← getStderr
-  liftM <| out.putStr <| toString s
+  out.putStr <| toString s
 
 def eprintln [ToString α] (s : α) : IO Unit :=
   eprint <| toString s |>.push '\n'
@@ -378,24 +365,13 @@ def eprintln [ToString α] (s : α) : IO Unit :=
 private def eprintlnAux (s : String) : IO Unit :=
   eprintln s
 
-def getEnv : String → m (Option String) := liftM ∘ Prim.getEnv
-
-def realPath : FilePath → m FilePath := liftM ∘ Prim.realPath
-def removeFile : FilePath → m Unit := liftM ∘ Prim.removeFile
-def appPath : m FilePath := liftM Prim.appPath
-
-def appDir : m FilePath := do
+def appDir : IO FilePath := do
   let p ← appPath
   let some p ← pure p.parent
-    | liftM (m := IO) <| throw <| IO.userError s!"System.IO.appDir: unexpected filename '{p}'"
-  realPath p
-
-def currentDir : m FilePath := liftM Prim.currentDir
-
-@[extern "lean_io_create_dir"]
-constant createDir : @& FilePath → IO Unit
+    | throw <| IO.userError s!"System.IO.appDir: unexpected filename '{p}'"
+  FS.realPath p
 
-partial def createDirAll (p : FilePath) : IO Unit := do
+partial def FS.createDirAll (p : FilePath) : IO Unit := do
   if ← p.isDir then
     return ()
   if let some parent := p.parent then
@@ -409,8 +385,6 @@ partial def createDirAll (p : FilePath) : IO Unit := do
       else
         throw e
 
-end
-
 namespace Process
 inductive Stdio where
   | piped
@@ -450,6 +424,15 @@ structure Child (cfg : StdioConfig) where
 
 @[extern "lean_io_process_child_wait"] constant Child.wait {cfg : @& StdioConfig} : @& Child cfg → IO UInt32
 
+/--
+Extract the `stdin` field from a `Child` object, allowing them to be freed independently.
+This operation is necessary for closing the child process' stdin while still holding on to a process handle,
+e.g. for `Child.wait`. A file handle is closed when all references to it are dropped, which without this
+operation includes the `Child` object.
+-/
+@[extern "lean_io_process_child_take_stdin"] constant Child.takeStdin {cfg : @& StdioConfig} : Child cfg →
+    IO (cfg.stdin.toHandleType × Child { cfg with stdin := Stdio.null })
+
 structure Output where
   exitCode : UInt32
   stdout   : String
@@ -468,9 +451,11 @@ def output (args : SpawnArgs) : IO Output := do
 def run (args : SpawnArgs) : IO String := do
   let out ← output args
   if out.exitCode != 0 then
-    throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode;
+    throw <| IO.userError <| "process '" ++ args.cmd ++ "' exited with code " ++ toString out.exitCode
   pure out.stdout
 
+@[extern "lean_io_exit"] constant exit : UInt8 → IO α
+
 end Process
 
 structure AccessRight where
@@ -508,7 +493,7 @@ instance : MonadLift (ST IO.RealWorld) (EIO ε) := ⟨fun x s =>
   | EStateM.Result.ok a s     => EStateM.Result.ok a s
   | EStateM.Result.error ex _ => nomatch ex⟩
 
-def mkRef [Monad m] [MonadLiftT (ST IO.RealWorld) m] (a : α) : m (IO.Ref α) :=
+def mkRef (a : α) : IO (IO.Ref α) :=
   ST.mkRef a
 
 namespace FS
@@ -516,12 +501,12 @@ namespace Stream
 
 @[export lean_stream_of_handle]
 def ofHandle (h : Handle) : Stream := {
-  isEof   := Prim.Handle.isEof h,
-  flush   := Prim.Handle.flush h,
-  read    := Prim.Handle.read h,
-  write   := Prim.Handle.write h,
-  getLine := Prim.Handle.getLine h,
-  putStr  := Prim.Handle.putStr h,
+  isEof   := Handle.isEof h,
+  flush   := Handle.flush h,
+  read    := Handle.read h,
+  write   := Handle.write h,
+  getLine := Handle.getLine h,
+  putStr  := Handle.putStr h,
 }
 
 structure Buffer where
@@ -550,14 +535,14 @@ def ofBuffer (r : Ref Buffer) : Stream := {
 end Stream
 
 /-- Run action with `stdin` emptied and `stdout+stderr` captured into a `String`. -/
-def withIsolatedStreams (x : IO α) : IO (String × Except IO.Error α) := do
+def withIsolatedStreams [Monad m] [MonadFinally m] [MonadExceptOf IO.Error m] [MonadLiftT IO m] (x : m α) : m (String × Except IO.Error α) := do
   let bIn ← mkRef { : Stream.Buffer }
   let bOut ← mkRef { : Stream.Buffer }
   let r ← withStdin (Stream.ofBuffer bIn) <|
     withStdout (Stream.ofBuffer bOut) <|
       withStderr (Stream.ofBuffer bOut) <|
         observing x
-  let bOut ← bOut.get
+  let bOut ← liftM (m := IO) bOut.get
   let out := String.fromUTF8Unchecked bOut.data
   pure (out, r)
 
@@ -571,7 +556,7 @@ namespace Lean
 /-- Typeclass used for presenting the output of an `#eval` command. -/
 class Eval (α : Type u) where
   -- We default `hideUnit` to `true`, but set it to `false` in the direct call from `#eval`
-  -- so that `()` output is hidden in chained instances such as for some `m Unit`.
+  -- so that `()` output is hidden in chained instances such as for some `IO Unit`.
   -- We take `Unit → α` instead of `α` because ‵α` may contain effectful debugging primitives (e.g., `dbg_trace`)
   eval : (Unit → α) → forall (hideUnit : optParam Bool true), IO Unit
 
diff --git a/src/Lean/Util/Path.lean b/src/Lean/Util/Path.lean
index 7be0af525704..a6c6ae843434 100644
--- a/src/Lean/Util/Path.lean
+++ b/src/Lean/Util/Path.lean
@@ -14,7 +14,7 @@ namespace Lean
 open System
 
 def realPathNormalized (p : FilePath) : IO FilePath := do
-  (← IO.realPath p).normalize
+  (← IO.FS.realPath p).normalize
 
 def modToFilePath (base : FilePath) (mod : Name) (ext : String) : FilePath :=
   go mod |>.withExtension ext
@@ -44,13 +44,20 @@ builtin_initialize searchPathRef : IO.Ref SearchPath ← IO.mkRef {}
 @[extern c inline "LEAN_IS_STAGE0"]
 private constant isStage0 (u : Unit) : Bool
 
-def getBuiltinSearchPath : IO SearchPath := do
-  let appDir ← IO.appDir
-  let mut buildDir := appDir / ".."
+@[export lean_get_prefix]
+def getBuildDir : IO FilePath := do
+  return (← IO.appDir).parent |>.get!
+
+@[export lean_get_libdir]
+def getLibDir : IO FilePath := do
+  let mut buildDir ← getBuildDir
   -- use stage1 stdlib with stage0 executable (which should never be distributed outside of the build directory)
   if isStage0 () then
     buildDir := buildDir / ".." / "stage1"
-  [buildDir / "lib" / "lean"]
+  buildDir / "lib" / "lean"
+
+def getBuiltinSearchPath : IO SearchPath :=
+  return [← getLibDir]
 
 def addSearchPathFromEnv (sp : SearchPath) : IO SearchPath := do
   let val ← IO.getEnv "LEAN_PATH"
@@ -88,7 +95,7 @@ partial def findOLean (mod : Name) : IO FilePath := do
 /-- Infer module name of source file name. -/
 @[export lean_module_name_of_file]
 def moduleNameOfFileName (fname : FilePath) (rootDir : Option FilePath) : IO Name := do
-  let fname ← IO.realPath fname
+  let fname ← IO.FS.realPath fname
   let rootDir ← match rootDir with
     | some rootDir => pure rootDir
     | none         => IO.currentDir
diff --git a/src/Leanpkg.lean b/src/Leanpkg.lean
index 74559d0344c7..101eb537e885 100644
--- a/src/Leanpkg.lean
+++ b/src/Leanpkg.lean
@@ -28,20 +28,20 @@ partial def withLockFile (x : IO α) : IO α := do
   try
     x
   finally
-    IO.removeFile lockFileName
+    IO.FS.removeFile lockFileName
   where
     acquire (firstTime := true) :=
       try
         -- TODO: lock file should ideally contain PID
         if !System.Platform.isWindows then
-          discard <| IO.Prim.Handle.mk lockFileName "wx"
+          discard <| IO.FS.Handle.mkPrim lockFileName "wx"
         else
           -- `x` mode doesn't seem to work on Windows even though it's listed at
           -- https://docs.microsoft.com/en-us/cpp/c-runtime-library/reference/fopen-wfopen?view=msvc-160
           -- ...? Let's use the slightly racy approach then.
           if ← lockFileName.pathExists then
             throw <| IO.Error.alreadyExists 0 ""
-          discard <| IO.Prim.Handle.mk lockFileName "w"
+          discard <| IO.FS.Handle.mk lockFileName IO.FS.Mode.write
       catch
         | IO.Error.alreadyExists _ _ => do
           if firstTime then
@@ -54,8 +54,8 @@ def getRootPart (pkg : FilePath := ".") : IO Lean.Name := do
   let entries ← pkg.readDir
   match entries.filter (FilePath.extension ·.fileName == "lean") with
   | #[rootFile] => FilePath.withExtension rootFile.fileName "" |>.toString
-  | #[]         => throw <| IO.userError s!"no '.lean' file found in {← IO.realPath "."}"
-  | _           => throw <| IO.userError s!"{← IO.realPath "."} must contain a unique '.lean' file as the package root"
+  | #[]         => throw <| IO.userError s!"no '.lean' file found in {← IO.FS.realPath "."}"
+  | _           => throw <| IO.userError s!"{← IO.FS.realPath "."} must contain a unique '.lean' file as the package root"
 
 structure Configuration :=
   leanPath    : String
diff --git a/src/Leanpkg/Build.lean b/src/Leanpkg/Build.lean
index 423f89023b25..82eacf75023c 100644
--- a/src/Leanpkg/Build.lean
+++ b/src/Leanpkg/Build.lean
@@ -75,8 +75,8 @@ partial def buildModule (mod : Name) : BuildM Result := do
       throw e
     try
       let cFile := modToFilePath tempBuildPath mod "c"
-      IO.createDirAll oleanFile.parent.get!
-      IO.createDirAll cFile.parent.get!
+      IO.FS.createDirAll oleanFile.parent.get!
+      IO.FS.createDirAll cFile.parent.get!
       execCmd {
         cmd := (← IO.appDir) / "lean" |>.withExtension FilePath.exeExtension |>.toString
         args := ctx.leanArgs.toArray ++ #["-o", oleanFile.toString, "-c", cFile.toString, leanFile.toString]
diff --git a/src/bin/leanc.in b/src/bin/leanc.in
index 3f415861d291..3212193b60ec 100755
--- a/src/bin/leanc.in
+++ b/src/bin/leanc.in
@@ -8,8 +8,8 @@
 #
 # Interesting options:
 # * `-U LEAN_MULTI_THREAD` can be used to optimize programs not making use of multi-threading
-# * `-print-cflags`: print C compiler flags necessary for building against the Lean runtime and abort
-# * `-print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and abort
+# * `--print-cflags`: print C compiler flags necessary for building against the Lean runtime and exit
+# * `--print-ldlags`: print C compiler flags necessary for statically linking against the Lean library and exit
 # * Set the `LEANC_GMP` environment variable to a path to `libgmp.a` (or `-l:libgmp.a` on Linux) to link GMP statically.
 #   Beware of the licensing consequences since GMP is LGPL.
 
@@ -25,8 +25,8 @@ for arg in "$@"; do
     [[ $arg == "-shared" ]] && ldflags_ext=(@LEANC_SHARED_LINKER_FLAGS@) && args=("-x" "c" "$@" "-x" "none")
     # Note the `-x c` for treating all input as C code
     [[ $arg == "-c" ]] && ldflags=() && ldflags_ext=() && args=("-x" "c" "$@" "-x" "none")
-    [[ $arg == "-print-cflags" ]] && echo "${cflags[@]}" && exit
-    [[ $arg == "-print-ldflags" ]] && echo "${cflags[@]} ${ldflags_ext[@]} ${ldflags[@]}" && exit
+    [[ $arg == "--print-cflags" ]] && echo "${cflags[@]}" && exit
+    [[ $arg == "--print-ldflags" ]] && echo "${cflags[@]} ${ldflags_ext[@]} ${ldflags[@]}" && exit
 done
 
 [ -n "$LEAN_CXX" ] || LEAN_CXX=c++
diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp
index 9d4c96f65341..8f8cecbe5e7b 100644
--- a/src/runtime/io.cpp
+++ b/src/runtime/io.cpp
@@ -837,6 +837,10 @@ extern "C" obj_res lean_io_wait_any(b_obj_arg task_list, obj_arg) {
     return io_result_mk_ok(v);
 }
 
+extern "C" obj_res lean_io_exit(obj_arg obj, obj_arg /* w */) {
+    exit((size_t) obj);
+}
+
 void initialize_io() {
     g_io_error_nullptr_read = mk_io_user_error(mk_string("null reference read"));
     mark_persistent(g_io_error_nullptr_read);
diff --git a/src/runtime/process.cpp b/src/runtime/process.cpp
index f0f6561fab00..294e942ad521 100644
--- a/src/runtime/process.cpp
+++ b/src/runtime/process.cpp
@@ -202,6 +202,13 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
     return lean_io_result_mk_ok(r.steal());
 }
 
+extern "C" obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
+    object_ref child(lchild);
+    object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), cnstr_get_ref(child, 3));
+    object_ref r = mk_cnstr(0, cnstr_get_ref(child, 0), child2);
+    return lean_io_result_mk_ok(r.steal());
+}
+
 void initialize_process() {
     g_win_handle_external_class = lean_register_external_class(win_handle_finalizer, win_handle_foreach);
 }
@@ -332,6 +339,14 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
     return lean_io_result_mk_ok(r.steal());
 }
 
+extern "C" obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
+    object_ref child(lchild);
+    object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), sizeof(pid_t));
+    cnstr_set_uint32(child2.raw(), 3 * sizeof(object *), cnstr_get_uint32(child.raw(), 3 * sizeof(object *)));
+    object_ref r = mk_cnstr(0, cnstr_get_ref(child, 0), child2);
+    return lean_io_result_mk_ok(r.steal());
+}
+
 void initialize_process() {}
 void finalize_process() {}
 
diff --git a/src/shell/lean.cpp b/src/shell/lean.cpp
index e4663e573329..3aa50ce909f2 100644
--- a/src/shell/lean.cpp
+++ b/src/shell/lean.cpp
@@ -203,6 +203,8 @@ static void display_help(std::ostream & out) {
 #endif
     std::cout << "  --plugin=file      load and initialize shared library for registering linters etc.\n";
     std::cout << "  --deps             just print dependencies of a Lean input\n";
+    std::cout << "  --print-prefix     print the installation prefix for Lean and exit\n";
+    std::cout << "  --print-libdir     print the installation directory for Lean's built-in libraries and exit\n";
     std::cout << "  --profile          display elaboration/type checking time for each definition/theorem\n";
     std::cout << "  --stats            display environment statistics\n";
     DEBUG_CODE(
@@ -211,6 +213,9 @@ static void display_help(std::ostream & out) {
     std::cout << "  -D name=value      set a configuration option (see set_option command)\n";
 }
 
+static int print_prefix = 0;
+static int print_libdir = 0;
+
 static struct option g_long_options[] = {
     {"version",      no_argument,       0, 'v'},
     {"help",         no_argument,       0, 'h'},
@@ -235,6 +240,8 @@ static struct option g_long_options[] = {
     {"worker",       no_argument,       0, 'W'},
 #endif
     {"plugin",       required_argument, 0, 'p'},
+    {"print-prefix", no_argument,       &print_prefix, 1},
+    {"print-libdir", no_argument,       &print_libdir, 1},
 #ifdef LEAN_DEBUG
     {"debug",        required_argument, 0, 'B'},
 #endif
@@ -303,7 +310,7 @@ void load_plugin(std::string path) {
     init = dlsym(handle, sym.c_str());
 #endif
     if (!init) {
-        throw exception(sstream() << "error, plugin " << path << " does not seem to contain a module '" << pkg << ".Default'");
+        throw exception(sstream() << "error, plugin " << path << " does not seem to contain a module '" << pkg << "'");
     }
     auto init_fn = reinterpret_cast<object *(*)(object *)>(init);
     object *r = init_fn(io_mk_world());
@@ -372,6 +379,9 @@ void environment_free_regions(environment && env) {
 }
 }
 
+extern "C" object * lean_get_prefix(object * w);
+extern "C" object * lean_get_libdir(object * w);
+
 void check_optarg(char const * option_name) {
     if (!optarg) {
         std::cerr << "error: argument missing for option '-" << option_name << "'" << std::endl;
@@ -440,6 +450,8 @@ int main(int argc, char ** argv) {
         int c = getopt_long(argc, argv, g_opt_str, g_long_options, NULL);
         if (c == -1)
             break; // end of command line
+        if (c == 0)
+            continue; // long-only option
         switch (c) {
             case 'e':
                 lean_set_exit_on_panic(true);
@@ -534,6 +546,16 @@ int main(int argc, char ** argv) {
         }
     }
 
+    if (print_prefix) {
+        std::cout << get_io_result<string_ref>(lean_get_prefix(io_mk_world())).data() << std::endl;
+        return 0;
+    }
+
+    if (print_libdir) {
+        std::cout << get_io_result<string_ref>(lean_get_libdir(io_mk_world())).data() << std::endl;
+        return 0;
+    }
+
     if (auto max_memory = opts.get_unsigned(get_max_memory_opt_name(),
                                             opts.get_bool("server") ? LEAN_SERVER_DEFAULT_MAX_MEMORY
                                                                     : LEAN_DEFAULT_MAX_MEMORY)) {
diff --git a/tests/compiler/foreign/Makefile b/tests/compiler/foreign/Makefile
index 819756cd4ad2..63601a2de38e 100644
--- a/tests/compiler/foreign/Makefile
+++ b/tests/compiler/foreign/Makefile
@@ -9,7 +9,7 @@ all: $(BIN_OUT)/test
 
 $(OUT)/testcpp/%.o: %.cpp
 	@mkdir -p "$(@D)"
-	c++ -std=c++14 -c -o $@ $< $(CPPFLAGS) `leanc -print-cflags`
+	c++ -std=c++14 -c -o $@ $< $(CPPFLAGS) `leanc --print-cflags`
 
 $(BIN_OUT)/test: $(LIB_OUT)/libmain.a $(CPP_OBJS) | $(BIN_OUT)
-	c++ -o $@ $^ `leanc -print-ldflags`
+	c++ -o $@ $^ `leanc --print-ldflags`
diff --git a/tests/lean/Process.lean b/tests/lean/Process.lean
index 6591d7226150..863a22350e85 100644
--- a/tests/lean/Process.lean
+++ b/tests/lean/Process.lean
@@ -47,3 +47,13 @@ def usingIO {α} (x : IO α) : IO α := x
 #eval usingIO do
   let child ← spawn { cmd := "sh", args := #["-c", "echo nullStderr >& 2"], stderr := Stdio.null };
   child.wait
+
+#eval usingIO do
+  let lean ← IO.Process.spawn {
+    cmd := "lean",
+    args := #["--stdin"]
+    stdin := IO.Process.Stdio.piped
+  }
+  let (stdin, lean) ← lean.takeStdin
+  stdin.putStr "#exit\n"
+  lean.wait
diff --git a/tests/lean/Process.lean.expected.out b/tests/lean/Process.lean.expected.out
index e17406597f2c..ad75179650c4 100644
--- a/tests/lean/Process.lean.expected.out
+++ b/tests/lean/Process.lean.expected.out
@@ -9,3 +9,4 @@ flush of broken pipe failed
 0
 0
 0
+0
diff --git a/tests/lean/doErrorMsg.lean.expected.out b/tests/lean/doErrorMsg.lean.expected.out
index 4c1a36742d7a..107b4ac83170 100644
--- a/tests/lean/doErrorMsg.lean.expected.out
+++ b/tests/lean/doErrorMsg.lean.expected.out
@@ -1,7 +1,7 @@
 doErrorMsg.lean:3:2-3:13: error: type mismatch
   IO.getStdin
 has type
-  EIO IO.Error IO.FS.Stream : Type
+  IO IO.FS.Stream : Type
 but is expected to have type
   IO PUnit : Type
 doErrorMsg.lean:15:19-15:21: error: type mismatch
diff --git a/tests/lean/doNotation1.lean.expected.out b/tests/lean/doNotation1.lean.expected.out
index 32b6253ca4fc..131fceda04d7 100644
--- a/tests/lean/doNotation1.lean.expected.out
+++ b/tests/lean/doNotation1.lean.expected.out
@@ -25,7 +25,7 @@ fun (x : Nat) => IO.println x
 doNotation1.lean:51:0-51:13: error: type mismatch
   IO.mkRef true
 has type
-  EIO IO.Error (IO.Ref Bool) : Type
+  IO (IO.Ref Bool) : Type
 but is expected to have type
   IO Unit : Type
 doNotation1.lean:58:2-58:20: error: type mismatch, result value has type