From cefc26d9cb356b0be241c75af3e8cf303e45f406 Mon Sep 17 00:00:00 2001 From: Gabriel Ebner Date: Tue, 11 Apr 2017 17:30:34 +0200 Subject: [PATCH] refactor(library/system/process): add exit status and working directory --- library/system/io.lean | 49 ++++++++++++++++++----- library/system/process.lean | 25 ------------ library/tools/smt2/default.lean | 1 - library/tools/smt2/solvers/z3.lean | 21 ++++------ src/library/process.cpp | 60 ++++++++++++++++++----------- src/library/process.h | 11 ++---- src/library/vm/vm_io.cpp | 52 ++++++++++++++++++++----- tests/lean/run/io_process_echo.lean | 3 -- 8 files changed, 131 insertions(+), 91 deletions(-) delete mode 100644 library/system/process.lean diff --git a/library/system/io.lean b/library/system/io.lean index a887616f01..d45e9a52b5 100644 --- a/library/system/io.lean +++ b/library/system/io.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Luke Nelson, Jared Roesch and Leonardo de Moura -/ import data.buffer -import system.process inductive io.error | other : string → io.error @@ -31,6 +30,30 @@ structure io.file_system (handle : Type) (m : Type → Type → Type) := (stdout : m io.error handle) (stderr : m io.error handle) +inductive io.process.stdio +| piped +| inherit +| null + +structure io.process.spawn_args := +/- Command name. -/ +(cmd : string) +/- Arguments for the process -/ +(args : list string := []) +/- Configuration for the process' stdin handle. -/ +(stdin := stdio.inherit) +/- Configuration for the process' stdout handle. -/ +(stdout := stdio.inherit) +/- Configuration for the process' stderr handle. -/ +(stderr := stdio.inherit) +/- Working directory for the process. -/ +(cwd : option string := none) + +structure io.process (handle : Type) (m : Type → Type → Type) := +(child : Type) (stdin : child → handle) (stdout : child → handle) (stderr : child → handle) +(spawn : io.process.spawn_args → m io.error child) +(wait : child → m io.error nat) + class io.interface := (m : Type → Type → Type) (monad : Π e, monad (m e)) @@ -42,7 +65,7 @@ class io.interface := -- Interface Extensions (term : io.terminal m) (fs : io.file_system handle m) -(process : io.process io.error handle m) +(process : io.process handle m) variable [io.interface] @@ -144,6 +167,16 @@ do h ← mk_file_handle s io.mode.read bin, c ← read h 1024, return $ some (r ++ c) end fs + +namespace proc +def child : Type := interface.process.child +def child.stdin : child → handle := interface.process.stdin +def child.stdout : child → handle := interface.process.stdout +def child.stderr : child → handle := interface.process.stderr +def spawn (p : io.process.spawn_args) : io child := interface.process.spawn p +def wait (c : child) : io nat := interface.process.wait c +end proc + end io meta constant format.print_using [io.interface] : format → options → io unit @@ -163,16 +196,14 @@ format.print (to_fmt a) read into `string` which is then returned. -/ def io.cmd [io.interface] (cmd : string) (args : list string) : io string := -do let proc : process := { +do child ← io.proc.spawn { cmd := cmd, args := args, - stdout := process.stdio.piped + stdout := io.process.stdio.piped }, - child ← interface.process.spawn proc, - let inh := child.stdin, - let outh := child.stdout, - let errh := child.stderr, - buf ← io.fs.read outh 1024, + buf ← io.fs.read child.stdout 1024, + exitv ← io.proc.wait child, + when (exitv ≠ 0) $ io.fail $ "process exited with status " ++ exitv.to_string, return buf.to_string /-- Lift a monadic `io` action into the `tactic` monad. -/ diff --git a/library/system/process.lean b/library/system/process.lean deleted file mode 100644 index d2dbb6aa99..0000000000 --- a/library/system/process.lean +++ /dev/null @@ -1,25 +0,0 @@ -import init.data.list.basic - -inductive process.stdio -| piped -| inherit -| null - -structure process := -(cmd : string) -/- Add an argument to pass to the process. -/ -(args : list string) -/- Configuration for the process's stdin handle. -/ -(stdin := stdio.inherit) -/- Configuration for the process's stdout handle. -/ -(stdout := stdio.inherit) -/- Configuration for the process's stderr handle. -/ -(stderr := stdio.inherit) - -structure process.child (handle : Type) := -(stdin : handle) -(stdout : handle) -(stderr : handle) - -structure io.process (err : Type) (handle : Type) (m : Type → Type → Type) := -(spawn : process → m err (process.child handle)) diff --git a/library/tools/smt2/default.lean b/library/tools/smt2/default.lean index dbd0133aa5..662ef29c0b 100644 --- a/library/tools/smt2/default.lean +++ b/library/tools/smt2/default.lean @@ -1,5 +1,4 @@ import system.io -import system.process import .solvers.z3 import .syntax import .builder diff --git a/library/tools/smt2/solvers/z3.lean b/library/tools/smt2/solvers/z3.lean index 17ab0020a2..86f58ab380 100644 --- a/library/tools/smt2/solvers/z3.lean +++ b/library/tools/smt2/solvers/z3.lean @@ -1,23 +1,16 @@ import system.io -import system.process import data.buffer -open process - structure z3_instance [io.interface] : Type := - (process : child io.handle) - -def spawn [ioi : io.interface] : process → io (child io.handle) := -io.interface.process.spawn + (process : io.proc.child) def z3_instance.start [io.interface] : io z3_instance := -do let proc : process := { - cmd := "z3", - args := ["-smt2", "-in"], - stdin := stdio.piped, - stdout := stdio.piped - }, - z3_instance.mk <$> spawn proc +z3_instance.mk <$> io.proc.spawn { + cmd := "z3", + args := ["-smt2", "-in"], + stdin := io.process.stdio.piped, + stdout := io.process.stdio.piped +} def z3_instance.raw [io.interface] (z3 : z3_instance) (cmd : string) : io string := do let z3_stdin := z3.process.stdin, diff --git a/src/library/process.cpp b/src/library/process.cpp index 3d0f940280..15a92e2c53 100644 --- a/src/library/process.cpp +++ b/src/library/process.cpp @@ -19,6 +19,7 @@ Author: Jared Roesch #include #else #include + #endif #include "library/process.h" @@ -51,6 +52,11 @@ process & process::set_stderr(stdio cfg) { return *this; } +process & process::set_cwd(std::string const &cwd) { + m_cwd = cwd; + return *this; +} + #if defined(LEAN_WINDOWS) && !defined(LEAN_CYGWIN) HANDLE to_win_handle(FILE * file) { @@ -92,6 +98,8 @@ static optional setup_stdio(SECURITY_ATTRIBUTES * saAttr, optional } } +// TODO(gabriel): add support for cwd parameter + // This code is adapted from: https://msdn.microsoft.com/en-us/library/windows/desktop/ms682499(v=vs.85).aspx child process::spawn() { HANDLE child_stdin = stdin; @@ -228,6 +236,11 @@ void process::run() { throw exception("process::run not supported on Windows"); } +unsigned child::wait() { + // TODO(gabriel): not implemented yet + return 0; +} + #else optional setup_stdio(optional cfg) { @@ -276,55 +289,58 @@ child process::spawn() { close(stderr_pipe->m_read_fd); } - buffer pargs; - - for (auto arg : this->m_args) { - auto str = new char[arg.size() + 1]; - arg.copy(str, arg.size()); - str[arg.size()] = '\0'; - pargs.push_back(str); + if (m_cwd) { + if (chdir(m_cwd->c_str()) < 0) { + std::cerr << "could not change directory to " << *m_cwd << std::endl; + exit(-1); + } } - pargs.data()[pargs.size()] = NULL; + buffer pargs; + for (auto & arg : m_args) + pargs.push_back(strdup(arg.c_str())); + pargs.push_back(NULL); - auto err = execvp(pargs.data()[0], pargs.data()); - if (err < 0) { - throw std::runtime_error("executing process failed: ..."); + if (execvp(pargs[0], pargs.data()) < 0) { + std::cerr << "could not execute external process" << std::endl; + exit(-1); } } else if (pid == -1) { throw std::runtime_error("forking process failed: ..."); } /* We want to setup the parent's view of the file descriptors. */ - int parent_stdin = STDIN_FILENO; - int parent_stdout = STDOUT_FILENO; - int parent_stderr = STDERR_FILENO; + FILE * parent_stdin = nullptr, * parent_stdout = nullptr, * parent_stderr = nullptr; if (stdin_pipe) { close(stdin_pipe->m_read_fd); - parent_stdin = stdin_pipe->m_write_fd; + parent_stdin = fdopen(stdin_pipe->m_write_fd, "w"); } if (stdout_pipe) { close(stdout_pipe->m_write_fd); - parent_stdout = stdout_pipe->m_read_fd; + parent_stdout = fdopen(stdout_pipe->m_read_fd, "r"); } if (stderr_pipe) { close(stderr_pipe->m_write_fd); - parent_stderr = stderr_pipe->m_read_fd; + parent_stderr = fdopen(stderr_pipe->m_read_fd, "r"); } return child(pid, - std::make_shared(fdopen(parent_stdin, "w")), - std::make_shared(fdopen(parent_stdout, "r")), - std::make_shared(fdopen(parent_stderr, "r"))); + std::make_shared(parent_stdin), + std::make_shared(parent_stdout), + std::make_shared(parent_stderr)); } void process::run() { - child ch = spawn(); + spawn().wait(); +} + +unsigned child::wait() { int status; - waitpid(ch.m_pid, &status, 0); + waitpid(m_pid, &status, 0); + return static_cast(WEXITSTATUS(status)); } #endif diff --git a/src/library/process.h b/src/library/process.h index 0c381d9e60..745e481e1b 100644 --- a/src/library/process.h +++ b/src/library/process.h @@ -38,7 +38,7 @@ struct child { m_stderr(hstderr), m_pid(pid) {} - void wait(); + unsigned wait(); }; class process { @@ -47,18 +47,15 @@ class process { optional m_stdout; optional m_stdin; optional m_stderr; + optional m_cwd; public: - process(process const & proc) : - m_proc_name(proc.m_proc_name), - m_args(proc.m_args), - m_stdout(proc.m_stdout), - m_stdin(proc.m_stdin), - m_stderr(proc.m_stderr) {} + process(process const & proc) = default; process(std::string exe_name); process & arg(std::string arg_str); process & set_stdin(stdio cfg); process & set_stdout(stdio cfg); process & set_stderr(stdio cfg); + process & set_cwd(std::string const & cwd); child spawn(); void run(); }; diff --git a/src/library/vm/vm_io.cpp b/src/library/vm/vm_io.cpp index 09fe8d6428..f42cc2cfd9 100644 --- a/src/library/vm/vm_io.cpp +++ b/src/library/vm/vm_io.cpp @@ -285,8 +285,26 @@ stdio to_stdio(vm_obj const & o) { } } +vm_obj to_obj(child const & ch) { + return mk_vm_constructor(0, { + mk_vm_nat(static_cast(ch.m_pid)), + to_obj(ch.m_stdin), + to_obj(ch.m_stdout), + to_obj(ch.m_stderr), + }); +} + +child to_child(vm_obj const & o) { + return child { + static_cast(to_unsigned(cfield(o, 0))), + to_handle(cfield(o, 1)), + to_handle(cfield(o, 2)), + to_handle(cfield(o, 3)), + }; +} + /* -structure process := +structure spawn_args := (cmd : string) /- Add an argument to pass to the process. -/ (args : list string) @@ -296,6 +314,7 @@ structure process := (stdout := stdio.inherit) /- Configuration for the process's stderr handle. -/ (stderr := stdio.inherit) + (cwd := option string) */ static vm_obj io_process_spawn(vm_obj const & process_obj, vm_obj const &) { std::string cmd = to_string(cfield(process_obj, 0)); @@ -307,6 +326,10 @@ 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 cwd; + if (!is_none(cfield(process_obj, 5))) + cwd = to_string(get_some_value(cfield(process_obj, 5))); + lean::process proc(cmd); for (auto arg : args) { @@ -317,24 +340,33 @@ static vm_obj io_process_spawn(vm_obj const & process_obj, vm_obj const &) { proc.set_stdout(stdout_stdio); proc.set_stderr(stderr_stdio); + if (cwd) proc.set_cwd(*cwd); + child ch = proc.spawn(); + return mk_io_result(to_obj(ch)); +} - auto child_obj = mk_vm_constructor(0, { - to_obj(ch.m_stdin), - to_obj(ch.m_stdout), - to_obj(ch.m_stderr) - }); - - // Should add helper functions for building real io.result - return mk_io_result(child_obj); +static vm_obj io_process_wait(vm_obj const & ch, vm_obj const &) { + return mk_io_result(mk_vm_nat(to_child(ch).wait())); } /* structure io.process (Err : Type) (handle : Type) (m : Type → Type → Type) := + (child : Type) + (stdin : child -> handle) + (stdout : child -> handle) + (stderr : child -> handle) (spawn : process → m Err child) + (wait : child -> m Err nat) */ static vm_obj mk_process() { - return mk_native_closure(io_process_spawn); + return mk_vm_constructor(0, { + mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c).m_stdin); }), + mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c).m_stdout); }), + mk_native_closure([] (vm_obj const & c) { return to_obj(to_child(c).m_stderr); }), + mk_native_closure(io_process_spawn), + mk_native_closure(io_process_wait), + }); } static vm_obj io_return(vm_obj const &, vm_obj const & a, vm_obj const &) { diff --git a/tests/lean/run/io_process_echo.lean b/tests/lean/run/io_process_echo.lean index 5aa496957e..18efafe8c4 100644 --- a/tests/lean/run/io_process_echo.lean +++ b/tests/lean/run/io_process_echo.lean @@ -1,7 +1,4 @@ import system.io -import system.process - -open process variable [io.interface]