diff --git a/src/Init/System/IO.lean b/src/Init/System/IO.lean index f84413cdf7..dfcbbad058 100644 --- a/src/Init/System/IO.lean +++ b/src/Init/System/IO.lean @@ -381,6 +381,23 @@ def appDir : m FilePath := do def currentDir : m FilePath := liftM Prim.currentDir +@[extern "lean_io_create_dir"] +constant createDir : @& FilePath → IO Unit + +partial def createDirAll (p : FilePath) : IO Unit := do + if ← p.isDir then + return () + if let some parent := p.parent then + createDirAll parent + try + createDir p + catch + | e => + if ← p.isDir then + pure () -- I guess someone else was faster + else + throw e + end namespace Process diff --git a/src/runtime/io.cpp b/src/runtime/io.cpp index ee30c239f0..a33b723a82 100644 --- a/src/runtime/io.cpp +++ b/src/runtime/io.cpp @@ -536,6 +536,18 @@ extern "C" obj_res lean_io_metadata(b_obj_arg fname, obj_arg) { return io_result_mk_ok(mdata); } +extern "C" obj_res lean_io_create_dir(b_obj_arg p, obj_arg) { +#ifdef LEAN_WINDOWS + if (mkdir(string_cstr(p)) == 0) { +#else + if (mkdir(string_cstr(p), 0777) == 0) { +#endif + return io_result_mk_ok(box(0)); + } else { + return io_result_mk_error(decode_io_error(errno, p)); + } +} + extern "C" obj_res lean_io_remove_file(b_obj_arg fname, obj_arg) { if (std::remove(string_cstr(fname)) == 0) { return io_result_mk_ok(box(0));