feat: IO.createDir, IO.createDirAll

This commit is contained in:
Sebastian Ullrich 2021-05-28 14:08:34 +02:00
parent 94aea76922
commit a9fa84815b
2 changed files with 29 additions and 0 deletions

View file

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

View file

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