Temp file utilities

Stream: lean4

[James Gallicchio]

I am in need of utilities for writing temp files in a threadsafe/atomic way. It also seems like something Lake would use. IMO there should be an API in IO.FS namespace for handling temp files.

Unix has a dedicated API for this; windows is a more complicated story. It seems like there is an atomic system call to create a new directory and fail if that directory already exists: https://stackoverflow.com/a/70958667 which we could make work

[Mario Carneiro]

James Gallicchio said:

and it looks like windows doesnt even have an API for atomically getting a unique temp file

The standard way to solve this problem is to use randomness. If you just stick a random string on the end of the temp file name then it will almost certainly not collide with an existing file