feat: Process.exit

Closes #356
This commit is contained in:
Daniel Selsam 2021-05-03 18:46:12 -07:00 committed by Leonardo de Moura
parent 4ed66cae3e
commit a22bba7bbf
2 changed files with 6 additions and 0 deletions

View file

@ -445,6 +445,8 @@ def run (args : SpawnArgs) : IO String := do
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

View file

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