FFI + impure invariants

Stream: lean4

[Henrik Böving]

I'm currently writing some Lean FFI code to the statvfs API which can operate on either a path (as a string) or a file descriptor. And of course if the path is invalid the Linux kernel will throw an error back at me for passing an invalid path. Now I do know there exists a function FilePath.pathExists : FilePath -> IO Bool so I was considering to have the Statvfs constructor that interacts with the API have a function that takes both a FilePath as well as a proof that the FilePath exists, or at least existed before we called into the constructor. But I'm not quite sure how to do this (or whether it is even doable) since pathExists is an impure function after all. Would somebody happen to have an idea for this type of function? (or whether this is even sensible to do)

[Xubai Wang]

The problem is that you cannot ensure that the file behind FilePath is not removed after 'pathExists' is called. My idea is to design a new LockedHandle type using the system file lock and have some axioms about it.

[Mac]

Alternatively, to handle race conditions without locks you can just recover from the error (i.e., catch it).