IO.FS.removeAll

Stream: lean4

[Mac]

While the Lean 4 core does have a native IO.FS.removeFile to delete a single file (which calls std::remove), it does not have an analogous native IO.FS.removeAll (which could call std::filesystem::remove_all or std::experimental::filesystem::remove_all for c++14) to recursively remove a directory. While this can be partially replicated in pure Lean, it has a number of pitfalls with race conditions that a native implementation would not.

Thus, the addition of such a function would be quite useful (it is needed in Lake for example). Since @Sebastian Ullrich added IO.FS.createDir (in #519) for leanpkg, I was wondering if an IO.FS.removeAll addition would be welcome (I might even be able to add it myself if need be).

[Mac]

Actually, it may not be currently possible to remove a directory at all from Lean since, unless I'm mistaken, std;:remove (and thus IO.FS.removeFile) can't delete directories at all (even empty ones).

[Sebastian Ullrich]

Mac said:

While this can be partially replicated in pure Lean, it has a number of pitfalls with race conditions that a native implementation would not.

Could you elaborate? The libstdc++ implementation looks straightforward/naive enough: https://code.woboq.org/gcc/libstdc++-v3/src/filesystem/ops.cc.html#1051

[Sebastian Ullrich]

Mac said:

Actually, it may not be currently possible to remove a directory at all from Lean since, unless I'm mistaken, std;:remove (and thus IO.FS.removeFile) can't delete directories at all (even empty ones).

Yes, we should add removeDir

[Mac]

Sebastian Ullrich said:

Could you elaborate? The libstdc++ implementation looks straightforward/naive enough: https://code.woboq.org/gcc/libstdc++-v3/src/filesystem/ops.cc.html#1051

Ah, yeah, my bad. I missed this part of the C++ filesystem library documentation yesterday:

The behavior is undefined if the calls to functions in this library introduce a file system race, that is, when multiple threads, processes, or computers interleave access and modification to the same object in a file system.

So, you are correct, the C++ implementation doesn't avoid races either. So, remove_all probably could just be replicated in Lean through the use of removeFile and (a new) removeDir.

[Sebastian Ullrich]

Gotta love a stdlib where deleting a directory can trigger undefined behavior