8.5. Files, File Handles, and Streams

Lean provides a consistent filesystem API on all supported platforms. These are the key concepts:

Files

Files are an abstraction provided by operating systems that provide random access to persistently-stored data, organized hierarchically into directories.

Directories

Directories, also known as folders, may contain files or other directories. Fundamentally, a directory maps names to the files and/or directories that it contains.

File Handles

File handles (Handle) are abstract references to files that have been opened for reading and/or writing. A file handle maintains a mode that determines whether reading and/or writing are allowed, along with a cursor that points at a specific location in the file. Reading from or writing to a file handle advances the cursor. File handles may be buffered, which means that reading from a file handle may not return the current contents of the persistent data, and writing to a file handle may not modify them immediately.

Paths

Files are primarily accessed via paths (System.FilePath). A path is a sequence of directory names, potentially terminated by a file name. They are represented by strings in which separator characters The current platform's separator characters are listed in System.FilePath.pathSeparators. delimit the names.

The details of paths are platform-specific. Absolute paths begin in a root directory; some operating systems have a single root, while others may have multiple root directories. Relative paths do not begin in a root directory and require that some other directory be taken as a starting point. In addition to directories, paths may contain the special directory names ., which refers to the directory in which it is found, and .., which refers to prior directory in the path.

Filenames, and thus paths, may end in one or more extensions that identify the file's type. Extensions are delimited by the character System.FilePath.extSeparator. On some platforms, executable files have a special extension (System.FilePath.exeExtension).

Streams

Streams are a higher-level abstraction over files, both providing additional functionality and hiding some details of files. While file handles are essentially a thin wrapper around the operating system's representation, streams are implemented in Lean as a structure called IO.FS.Stream. Because streams are implemented in Lean, user code can create additional streams, which can be used seamlessly together with those provided in the standard library.

8.5.1. Low-Level File API

At the lowest level, files are explicitly opened using Handle.mk. When the last reference to the handle object is dropped, the file is closed. There is no explicit way to close a file handle other than by ensuring that there are no references to it.

opaque

IO.FS.Handle : Type

opaque

IO.FS.Handle.mk (fn : System.FilePath)
    (mode : IO.FS.Mode) : IO IO.FS.Handle

inductive type

IO.FS.Mode : Type

The mode of a file handle (i.e., a set of open flags and an fdopen mode).

All modes do not translate line endings (i.e., O_BINARY on Windows) and are not inherited across process creation (i.e., O_NOINHERIT on Windows, O_CLOEXEC elsewhere).

References:

Windows: _open, _fdopen
Linux: open, fdopen

Constructors

read : IO.FS.Mode
File opened for reading. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.
- open flags: O_RDONLY
- fdopen mode: r
write : IO.FS.Mode
File opened for writing. On open, truncate an existing file to zero length or create a new file. The stream is positioned at the beginning of the file.
- open flags: O_WRONLY | O_CREAT | O_TRUNC
- fdopen mode: w
writeNew : IO.FS.Mode
New file opened for writing. On open, create a new file with the stream positioned at the start. Errors if the file already exists.
- open flags: O_WRONLY | O_CREAT | O_TRUNC | O_EXCL
- fdopen mode: w
readWrite : IO.FS.Mode
File opened for reading and writing. On open, the stream is positioned at the beginning of the file. Errors if the file does not exist.
- open flags: O_RDWR
- fdopen mode: r+
append : IO.FS.Mode
File opened for writing. On open, create a new file if it does not exist. The stream is positioned at the end of the file.
- open flags: O_WRONLY | O_CREAT | O_APPEND
- fdopen mode: a

opaque

IO.FS.Handle.read (h : IO.FS.Handle)
    (bytes : USize) : IO ByteArray

Read up to the given number of bytes from the handle. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

def

IO.FS.Handle.readToEnd (h : IO.FS.Handle)
    : IO String

def

IO.FS.Handle.readBinToEnd (h : IO.FS.Handle)
    : IO ByteArray

def

IO.FS.Handle.readBinToEndInto (h : IO.FS.Handle)
    (buf : ByteArray) : IO ByteArray

opaque

IO.FS.Handle.getLine (h : IO.FS.Handle)
    : IO String

Read text up to (including) the next line break from the handle. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a handle, so further reads may block and return more data.

opaque

IO.FS.Handle.write (h : IO.FS.Handle)
    (buffer : ByteArray) : IO Unit

opaque

IO.FS.Handle.putStr (h : IO.FS.Handle)
    (s : String) : IO Unit

def

IO.FS.Handle.putStrLn (h : IO.FS.Handle)
    (s : String) : IO Unit

opaque

IO.FS.Handle.flush (h : IO.FS.Handle) : IO Unit

opaque

IO.FS.Handle.rewind (h : IO.FS.Handle) : IO Unit

Rewinds the read/write cursor to the beginning of the handle.

opaque

IO.FS.Handle.truncate (h : IO.FS.Handle)
    : IO Unit

Truncates the handle to the read/write cursor.

Does not automatically flush. Usually this is fine because the read/write cursor includes buffered writes. However, the combination of buffered writes, then rewind, then truncate, then close may lead to a file with content. If unsure, flush before truncating.

opaque

IO.FS.Handle.isTty (h : IO.FS.Handle)
    : BaseIO Bool

Returns true if a handle refers to a Windows console or Unix terminal.

opaque

IO.FS.Handle.lock (h : IO.FS.Handle)
  (exclusive : Bool := true) : IO Unit

Acquires an exclusive or shared lock on the handle. Will block to wait for the lock if necessary.

NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

opaque

IO.FS.Handle.tryLock (h : IO.FS.Handle)
  (exclusive : Bool := true) : IO Bool

Tries to acquire an exclusive or shared lock on the handle. Will NOT block for the lock, but instead return false.

NOTE: Acquiring a exclusive lock while already possessing a shared lock will NOT reliably succeed (i.e., it works on Unix but not on Windows).

opaque

IO.FS.Handle.unlock (h : IO.FS.Handle) : IO Unit

Releases any previously acquired lock on the handle. Will succeed even if no lock has been acquired.

One File, Multiple Handles

This program has two handles to the same file. Because file I/O may be buffered independently for each handle, Handle.flush should be called when the buffers need to be synchronized with the file's actual contents. Here, the two handles proceed in lock-step through the file, with one of them a single byte ahead of the other. The first handle is used to count the number of occurrences of 'A', while the second is used to replace each 'A' with '!'. The second handle is opened in readWrite mode rather than write mode because opening an existing file in write mode replaces it with an empty file. In this case, the buffers don't need to be flushed during execution because modifications occur only to parts of the file that will not be read again, but the write handle should be flushed after the loop has completed.

open IO.FS (Handle)

def main : IO Unit := do
  IO.println s!"Starting contents: '{(← IO.FS.readFile "data").trim}'"

  let h ← Handle.mk "data" .read
  let h' ← Handle.mk "data" .readWrite
  h'.rewind

  let mut count := 0
  let mut buf : ByteArray ← h.read 1
  while ok : buf.size = 1 do
    if Char.ofUInt8 buf[0] == 'A' then
      count := count + 1
      h'.write (ByteArray.empty.push '!'.toUInt8)
    else
      h'.write buf
    buf ← h.read 1

  h'.flush

  IO.println s!"Count: {count}"
  IO.println s!"Contents: '{(← IO.FS.readFile "data").trim}'"

When run on this file:

Input: dataAABAABCDAB

the program outputs:

stdoutStarting contents: 'AABAABCDAB'Count: 5Contents: '!!B!!BCD!B'

Afterwards, the file contains:

Output: data!!B!!BCD!B

8.5.2. Streams

structure

IO.FS.Stream : Type

A pure-Lean abstraction of POSIX streams. We use Streams for the standard streams stdin/stdout/stderr so we can capture output of #eval commands into memory.

Constructor

IO.FS.Stream.mk

Fields

`flush`	`:`	`IO Unit`
`read`	`:`	`USize → IO ByteArray`
		Read up to the given number of bytes from the stream. If the returned array is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.
`write`	`:`	`ByteArray → IO Unit`
`getLine`	`:`	`IO String`
		Read text up to (including) the next line break from the stream. If the returned string is empty, an end-of-file marker has been reached. Note that EOF does not actually close a stream, so further reads may block and return more data.
`putStr`	`:`	`String → IO Unit`
`isTty`	`:`	`BaseIO Bool`
		Returns true if a stream refers to a Windows console or Unix terminal.

def

IO.FS.withIsolatedStreams.{u_1}
  {m : Type → Type u_1} {α : Type} [Monad m]
  [MonadFinally m] [MonadLiftT BaseIO m]
  (x : m α) (isolateStderr : Bool := true) :
  m (String × α)

Run action with stdin emptied and stdout+stderr captured into a String.

def

IO.FS.Stream.ofBuffer
    (r : IO.Ref IO.FS.Stream.Buffer)
    : IO.FS.Stream

def

IO.FS.Stream.ofHandle (h : IO.FS.Handle)
    : IO.FS.Stream

def

IO.FS.Stream.putStrLn (strm : IO.FS.Stream)
    (s : String) : IO Unit

structure

IO.FS.Stream.Buffer : Type

Constructor

IO.FS.Stream.Buffer.mk

Fields

`data`	`:`	`ByteArray`
`pos`	`:`	`Nat`

def

IO.FS.Stream.Buffer.data
    (self : IO.FS.Stream.Buffer) : ByteArray

def

IO.FS.Stream.Buffer.pos
    (self : IO.FS.Stream.Buffer) : Nat

8.5.3. Paths

Paths are represented by strings. Different platforms have different conventions for paths: some use slashes (/) as directory separators, others use backslashes (\). Some are case-sensitive, others are not. Different Unicode encodings and normal forms may be used to represent filenames, and some platforms consider filenames to be byte sequences rather than strings. A string that represents an absolute path on one system may not even be a valid path on another system.

To write Lean code that is as compatible as possible with multiple systems, it can be helpful to use Lean's path manipulation primitives instead of raw string manipulation. Helpers such as System.FilePath.join take platform-specific rules for absolute paths into account, System.FilePath.pathSeparator contains the appropriate path separator for the current platform, and System.FilePath.exeExtension contains any necessary extension for executable files. Avoid hard-coding these rules.

There is an instance of the Div type class for FilePath which allows the slash operator to be used to concatenate paths.

structure

System.FilePath : Type

Constructor

System.FilePath.mk

Fields

toString : String

def

System.mkFilePath (parts : List String)
    : System.FilePath

def

System.FilePath.join (p sub : System.FilePath)
    : System.FilePath

def

System.FilePath.normalize (p : System.FilePath)
    : System.FilePath

def

System.FilePath.isAbsolute (p : System.FilePath)
    : Bool

def

System.FilePath.isRelative (p : System.FilePath)
    : Bool

def

System.FilePath.parent (p : System.FilePath)
    : Option System.FilePath

def

System.FilePath.components (p : System.FilePath)
    : List String

def

System.FilePath.fileName (p : System.FilePath)
    : Option String

def

System.FilePath.fileStem (p : System.FilePath)
    : Option String

Extracts the stem (non-extension) part of p.fileName.

def

System.FilePath.extension (p : System.FilePath)
    : Option String

def

System.FilePath.addExtension
    (p : System.FilePath) (ext : String)
    : System.FilePath

Appends the extension ext to a path p.

ext should not contain a leading ., as this function adds one. If ext is the empty string, no . is added.

Unlike System.FilePath.withExtension, this does not remove any existing extension.

def

System.FilePath.withExtension
    (p : System.FilePath) (ext : String)
    : System.FilePath

Replace the current extension in a path p with ext.

ext should not contain a ., as this function adds one. If ext is the empty string, no . is added.

def

System.FilePath.withFileName
    (p : System.FilePath) (fname : String)
    : System.FilePath

def

System.FilePath.pathSeparator : Char

The character that separates directories. In the case where more than one character is possible, pathSeparator is the 'ideal' one.

def

System.FilePath.pathSeparators : List Char

The list of all possible separators.

def

System.FilePath.extSeparator : Char

File extension character

def

System.FilePath.exeExtension : String

8.5.4. Interacting with the Filesystem

Some operations on paths consult the filesystem.

structure

IO.FS.Metadata : Type

Constructor

IO.FS.Metadata.mk

Fields

`accessed`	`:`	`IO.FS.SystemTime`
`modified`	`:`	`IO.FS.SystemTime`
`byteSize`	`:`	`UInt64`
`type`	`:`	`IO.FS.FileType`

opaque

System.FilePath.metadata
    : System.FilePath → IO IO.FS.Metadata

def

System.FilePath.pathExists (p : System.FilePath)
    : BaseIO Bool

def

System.FilePath.isDir (p : System.FilePath)
    : BaseIO Bool

structure

IO.FS.DirEntry : Type

Constructor

IO.FS.DirEntry.mk

Fields

`root`	`:`	`System.FilePath`
`fileName`	`:`	`String`

def

IO.FS.DirEntry.path (entry : IO.FS.DirEntry)
    : System.FilePath

opaque

System.FilePath.readDir
    : System.FilePath →
      IO (Array IO.FS.DirEntry)

def

System.FilePath.walkDir (p : System.FilePath)
  (enter : System.FilePath → IO Bool := fun x =>
    pure true) :
  IO (Array System.FilePath)

Return all filesystem entries of a preorder traversal of all directories satisfying enter, starting at p. Symbolic links are visited as well by default.

structure

IO.FileRight : Type

Constructor

IO.FileRight.mk

Fields

`user`	`:`	`IO.AccessRight`
`group`	`:`	`IO.AccessRight`
`other`	`:`	`IO.AccessRight`

def

IO.FileRight.flags (acc : IO.FileRight) : UInt32

def

IO.setAccessRights (filename : System.FilePath)
    (mode : IO.FileRight) : IO Unit

opaque

IO.FS.removeFile (fname : System.FilePath)
    : IO Unit

opaque

IO.FS.rename (old new : System.FilePath)
    : IO Unit

Moves a file or directory old to the new location new.

This function coincides with the POSIX rename function, see there for more information.

opaque

IO.FS.removeDir : System.FilePath → IO Unit

Remove given directory. Fails if not empty; see also IO.FS.removeDirAll.

def

IO.FS.lines (fname : System.FilePath)
    : IO (Array String)

def

IO.FS.withTempFile.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT IO m]
    (f : IO.FS.Handle → System.FilePath → m α)
    : m α

Like createTempFile, but also takes care of removing the file after usage.

opaque

IO.FS.createDirAll (p : System.FilePath)
    : IO Unit

Create given path and all missing parents as directories.

def

IO.FS.writeBinFile (fname : System.FilePath)
    (content : ByteArray) : IO Unit

def

IO.FS.withFile {α : Type} (fn : System.FilePath)
    (mode : IO.FS.Mode)
    (f : IO.FS.Handle → IO α) : IO α

opaque

IO.FS.removeDirAll (p : System.FilePath)
    : IO Unit

Fully remove given directory by deleting all contained files and directories in an unspecified order. Fails if any contained entry cannot be deleted or was newly created during execution.

opaque

IO.FS.createTempFile
    : IO (IO.FS.Handle × System.FilePath)

Creates a temporary file in the most secure manner possible. There are no race conditions in the file’s creation. The file is readable and writable only by the creating user ID. Additionally on UNIX style platforms the file is executable by nobody. The function returns both a Handle to the already opened file as well as its FilePath.

Note that it is the caller's job to remove the file after use.

def

IO.FS.readFile (fname : System.FilePath)
    : IO String

opaque

IO.FS.realPath (fname : System.FilePath)
    : IO System.FilePath

Resolves a pathname to an absolute pathname with no '.', '..', or symbolic links.

This function coincides with the POSIX realpath function, see there for more information.

def

IO.FS.writeFile (fname : System.FilePath)
    (content : String) : IO Unit

def

IO.FS.readBinFile (fname : System.FilePath)
    : IO ByteArray

opaque

IO.FS.createDir : System.FilePath → IO Unit

8.5.5. Standard I/O🔗

On operating systems that are derived from or inspired by Unix, standard input, standard output, and standard error are the names of three streams that are available in each process. Generally, programs are expected to read from standard input, write ordinary output to the standard output, and error messages to the standard error. By default, standard input receives input from the console, while standard output and standard error output to the console, but all three are often redirected to or from pipes or files.

Rather than providing direct access to the operating system's standard I/O facilities, Lean wraps them in Streams. Additionally, the IO monad contains special support for replacing or locally overriding them. This extra level of indirection makes it possible to redirect input and output within a Lean program.

opaque

IO.getStdin : BaseIO IO.FS.Stream

Reading from Standard Input

In this example, IO.getStdin and IO.getStdout are used to get the current standard input and output, respectively. These can be read from and written to.

def main : IO Unit := do
  let stdin ← IO.getStdin
  let stdout ← IO.getStdout
  stdout.putStrLn "Who is it?"
  let name ← stdin.getLine
  stdout.putStr "Hello, "
  stdout.putStrLn name

With this standard input:

stdinLean user

the standard output is:

stdoutWho is it?Hello, Lean user

opaque

IO.setStdin : IO.FS.Stream → BaseIO IO.FS.Stream

Replaces the stdin stream of the current thread and returns its previous value.

def

IO.withStdin.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT BaseIO m] (h : IO.FS.Stream)
    (x : m α) : m α

opaque

IO.getStdout : BaseIO IO.FS.Stream

opaque

IO.setStdout
    : IO.FS.Stream → BaseIO IO.FS.Stream

Replaces the stdout stream of the current thread and returns its previous value.

def

IO.withStdout.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT BaseIO m] (h : IO.FS.Stream)
    (x : m α) : m α

opaque

IO.getStderr : BaseIO IO.FS.Stream

opaque

IO.setStderr
    : IO.FS.Stream → BaseIO IO.FS.Stream

Replaces the stderr stream of the current thread and returns its previous value.

def

IO.withStderr.{u_1} {m : Type → Type u_1}
    {α : Type} [Monad m] [MonadFinally m]
    [MonadLiftT BaseIO m] (h : IO.FS.Stream)
    (x : m α) : m α

def

IO.FS.withIsolatedStreams.{u_1}
  {m : Type → Type u_1} {α : Type} [Monad m]
  [MonadFinally m] [MonadLiftT BaseIO m]
  (x : m α) (isolateStderr : Bool := true) :
  m (String × α)

Run action with stdin emptied and stdout+stderr captured into a String.

Redirecting Standard I/O to Strings

The countdown function counts down from a specified number, writing its progress to standard output. Using IO.FS.withIsolatedStreams, this output can be redirected to a string.

def countdown : Nat → IO Unit
  | 0 =>
    IO.println "Blastoff!"
  | n + 1 => do
    IO.println s!"{n + 1}"
    countdown n

def runCountdown : IO String := do
  let (output, ()) ← IO.FS.withIsolatedStreams (countdown 10)
  return output

"10\n9\n8\n7\n6\n5\n4\n3\n2\n1\nBlastoff!\n"#eval runCountdown

Running countdown yields a string that contains the output:

"10\n9\n8\n7\n6\n5\n4\n3\n2\n1\nBlastoff!\n"

8.5.6. Files and Directories

opaque

IO.currentDir : IO System.FilePath

opaque

IO.appPath : IO System.FilePath

def

IO.appDir : IO System.FilePath