21.5. 文件、文件句柄和流🔗

Lean 在所有支持的平台上提供一致的文件系统 API。这些是关键概念：

文件

文件是操作系统提供的一种抽象，它提供对持久存储的数据的随机访问，这些数据按层次结构组织到目录中。

目录

目录，也称为文件夹，可能包含文件或其他目录。从根本上来说，目录将名称映射到它包含的文件和/或目录。

文件句柄

文件句柄 (Handle) 是对已打开以进行读取和/或写入的文件的抽象引用。文件句柄维护一种确定是否允许读取和/或写入的模式，以及指向文件中特定位置的光标。读取或写入文件句柄会使光标前进。文件句柄可能是 buffered，这意味着从文件句柄读取可能不会返回持久数据的当前内容，并且写入文件句柄可能不会立即修改它们。

路径

文件主要通过 paths (System.FilePath) 访问。路径是目录名的序列，可能以文件名结尾。它们由字符串表示，其中分隔符当前平台的分隔符在 System.FilePath.pathSeparators 中列出。分隔名称。

路径的详细信息是特定于平台的。绝对路径从 根目录 开始；某些操作系统具有单个根目录，而其他操作系统可能具有多个根目录。相对路径不从根目录开始，并且需要将某个其他目录作为起点。除了目录之外，路径还可以包含特殊目录名称 .（指在其中找到它的目录）和 ..（指路径中先前的目录）。

文件名和路径可能以一个或多个标识文件类型的 extensions 结尾。扩展名由字符 System.FilePath.extSeparator 分隔。在某些平台上，可执行文件具有特殊扩展名 (System.FilePath.exeExtension)。

流

流是对文件的更高级别的抽象，既提供附加功能又隐藏文件的一些细节。虽然文件句柄本质上是围绕操作系统表示的薄包装器，但流在 Lean 中实现为称为 IO.FS.Stream 的结构。由于流是在 Lean 中实现的，因此用户代码可以创建额外的流，这些流可以与标准库中提供的流无缝地一起使用。

21.5.1. 低级文件 API🔗

在最低级别，文件是使用 Handle.mk 显式打开的。当删除对句柄对象的最后一个引用时，文件将被关闭。除了确保没有对文件句柄的引用之外，没有明确的方法可以关闭文件句柄。

opaque

IO.FS.Handle : Type
IO.FS.Handle : Type

A reference to an opened file.

File handles wrap the underlying operating system's file descriptors. There is no explicit operation to close a file: when the last reference to a file handle is dropped, the file is closed automatically.

Handles have an associated read/write cursor that determines where reads and writes occur in the file.

opaque

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

Opens the file at fn with the given mode.

An exception is thrown if the file cannot be opened.

inductive type

IO.FS.Mode : Type
IO.FS.Mode : Type

Whether a file should be opened for reading, writing, creation and writing, or appending.

At the operating system level, this translates to the mode of a file handle (i.e., a set of open flags and an fdopen mode).

None of the modes represented by this datatype translate line endings (i.e. O_BINARY on Windows). Furthermore, they are not inherited across process creation (i.e. O_NOINHERIT on Windows and O_CLOEXEC elsewhere).

Operating System Specifics:

Windows: _open, _fdopen
Linux: open, fdopen

Constructors

IO.FS.Mode.read : IO.FS.Mode

The file should be opened for reading.

The read/write cursor is positioned at the beginning of the file. It is an error if the file does not exist.

open flags: O_RDONLY
fdopen mode: r

IO.FS.Mode.write : IO.FS.Mode

The file should be opened for writing.

If the file already exists, it is truncated to zero length. Otherwise, a new file is created. The read/write cursor is positioned at the beginning of the file.

open flags: O_WRONLY | O_CREAT | O_TRUNC
fdopen mode: w

IO.FS.Mode.writeNew : IO.FS.Mode

A new file should be created for writing.

It is an error if the file already exists. A new file is created, with the read/write cursor positioned at the start.

open flags: O_WRONLY | O_CREAT | O_TRUNC | O_EXCL
fdopen mode: w

IO.FS.Mode.readWrite : IO.FS.Mode

The file should be opened for both reading and writing.

It is an error if the file does not already exist. The read/write cursor is positioned at the start of the file.

open flags: O_RDWR
fdopen mode: r+

IO.FS.Mode.append : IO.FS.Mode

The file should be opened for writing.

If the file does not already exist, it is created. If the file already exists, it is opened, and the read/write cursor 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
IO.FS.Handle.read (h : IO.FS.Handle)
  (bytes : USize) : IO ByteArray

Reads up to the given number of bytes from the handle. If the returned array is empty, an end-of-file marker (EOF) has been reached.

Encountering an EOF does not close a handle. Subsequent reads may block and return more data.

def

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

Reads the entire remaining contents of the file handle as a UTF-8-encoded string. An exception is thrown if the contents are not valid UTF-8.

The underlying file is not automatically closed, and subsequent reads from the handle may block and/or return data.

def

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

Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is encountered.

The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from the handle may block and/or return data.

def

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

Reads the entire remaining contents of the file handle until an end-of-file marker (EOF) is encountered.

The underlying file is not automatically closed upon encountering an EOF, and subsequent reads from the handle may block and/or return data.

opaque

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

Reads UTF-8-encoded text up to and including the next line break from the handle. If the returned string is empty, an end-of-file marker (EOF) has been reached.

Encountering an EOF does not close a handle. Subsequent reads may block and return more data.

opaque

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

Writes the provided bytes to the handle.

Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use IO.FS.Handle.flush to write changes to buffers to the associated device.

opaque

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

Writes the provided string to the file handle using the UTF-8 encoding.

Writing to a handle is typically buffered, and may not immediately modify the file on disk. Use IO.FS.Handle.flush to write changes to buffers to the associated device.

def

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

Writes the contents of the string to the handle, followed by a newline. Uses UTF-8.

opaque

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

Flushes the output buffer associated with the handle, writing any unwritten data to the associated output device.

opaque

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

Rewinds the read/write cursor to the beginning of the handle's file.

opaque

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

Truncates the handle to its read/write cursor.

This operation does not automatically flush output buffers, so the contents of the output device may not reflect the change immediately. This does not usually lead to problems because the read/write cursor includes buffered writes. However, buffered writes followed by IO.FS.Handle.rewind, then IO.FS.Handle.truncate, and then closing the file may lead to a non-empty file. If unsure, call IO.FS.Handle.flush before truncating.

opaque

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

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

opaque

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

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

Acquiring an exclusive lock while already possessing a shared lock will not reliably succeed: it works on Unix-like systems but not on Windows.

opaque

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

Tries to acquire an exclusive or shared lock on the handle and returns true if successful. Will not block if the lock cannot be acquired, but instead returns false.

Acquiring an exclusive lock while already possessing a shared lock will not reliably succeed: it works on Unix-like systems but not on Windows.

opaque

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

Releases any previously-acquired lock on the handle. Succeeds even if no lock has been acquired.

One File, Multiple Handles

该程序对同一文件有两个句柄。由于文件 I/O 可能会针对每个句柄独立缓冲，因此当缓冲区需要与文件的实际内容同步时，应调用 Handle.flush。在这里，两个句柄以锁步方式处理文件，其中一个句柄比另一个句柄领先一个字节。第一个句柄用于计算 'A' 出现的次数，而第二个句柄用于将每个 'A' 替换为 '!'。第二个句柄在 readWrite 模式而不是 write 模式下打开，因为在 write 模式下打开现有文件会将其替换为空文件。在这种情况下，在执行期间不需要刷新缓冲区，因为修改仅发生在不会再次读取的文件部分，但应在循环完成后刷新写入句柄。

open IO.FS (Handle)

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

  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").trimAscii}'"

当运行此文件时：

Input: dataAABAABCDAB

程序输出：

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

之后，该文件包含：

Output: data!!B!!BCD!B

21.5.2. 流🔗

structure

IO.FS.Stream : Type
IO.FS.Stream : Type

A pure-Lean abstraction of POSIX streams. These streams may represent an underlying POSIX stream or be implemented by Lean code.

Because standard input, standard output, and standard error are all IO.FS.Streams that can be overridden, Lean code may capture and redirect input and output.

Constructor

IO.FS.Stream.mk

Fields

flush : IO Unit

Flushes the stream's output buffers.

read : USize → IO ByteArray

Reads up to the given number of bytes from the stream.

If the returned array is empty, an end-of-file marker (EOF) has been reached. An EOF does not actually close a stream, so further reads may block and return more data.

write : ByteArray → IO Unit

Writes the provided bytes to the stream.

If the stream represents a physical output device such as a file on disk, then the results may be buffered. Call FS.Stream.flush to synchronize their contents.

getLine : IO String

Reads text up to and including the next newline from the stream.

If the returned string is empty, an end-of-file marker (EOF) has been reached. An EOF does not actually close a stream, so further reads may block and return more data.

putStr : String → IO Unit

Writes the provided string to the stream.

isTty : BaseIO Bool

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

def

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

Creates a stream from a mutable reference to a buffer.

The resulting stream simulates a file, mutating the contents of the reference in response to writes and reading from it in response to reads. These streams can be used with IO.withStdin, IO.setStdin, and the corresponding operators for standard output and standard error to redirect input and output.

def

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

Creates a Lean stream from a file handle. Each stream operation is implemented by the corresponding file handle operation.

def

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

Writes the contents of the string to the stream, followed by a newline.

structure

IO.FS.Stream.Buffer : Type
IO.FS.Stream.Buffer : Type

A byte buffer that can simulate a file in memory.

Use IO.FS.Stream.ofBuffer to create a stream from a buffer.

Constructor

IO.FS.Stream.Buffer.mk

Fields

data : ByteArray

The contents of the buffer.

pos : Nat

The read/write cursor's position in the buffer.

21.5.3. 路径🔗

路径由字符串表示。不同的平台对路径有不同的约定：一些使用斜杠（/）作为目录分隔符，另一些使用反斜杠（\）。有些区分大小写，有些则不区分大小写。可以使用不同的 Unicode 编码和正常形式来表示文件名，并且某些平台将文件名视为字节序列而不是字符串。在一个系统上表示绝对路径的字符串在另一系统上甚至可能不是有效路径。

要编写与多个系统尽可能兼容的 Lean 代码，使用 Lean 的路径操作原语而不是原始字符串操作会很有帮助。 System.FilePath.join 等帮助程序会考虑绝对路径的特定于平台的规则，System.FilePath.pathSeparator 包含当前平台的适当路径分隔符，System.FilePath.exeExtension 包含可执行文件的任何必要扩展名。避免对这些规则进行硬编码。

FilePath 有一个 Div 类型类的实例，它允许使用斜杠运算符来连接路径。

structure

System.FilePath : Type
System.FilePath : Type

A path on the file system.

Paths consist of a sequence of directories followed by the name of a file or directory. They are delimited by a platform-dependent separator character (see System.FilePath.pathSeparator).

Constructor

System.FilePath.mk

Fields

toString : String

The string representation of the path.

def

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

Constructs a path from a list of file names by interspersing them with the current platform's path separator.

def

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

Appends two paths, taking absolute paths into account. This operation is also accessible via the / operator.

If sub is an absolute path, then p is discarded and sub is returned. If sub is a relative path, then it is attached to p with the platform-specific path separator.

def

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

Normalizes a path, returning an equivalent path that may better follow platform conventions.

In particular:

On Windows, drive letters are made uppercase.
On platforms that support multiple path separators (that is, where System.FilePath.pathSeparators has length greater than one), alternative path separators are replaced with the preferred path separator.

There is no guarantee that two equivalent paths normalize to the same path.

def

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

An absolute path starts at the root directory or a drive letter. Accessing files through an absolute path does not depend on the current working directory.

def

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

A relative path is one that depends on the current working directory for interpretation. Relative paths do not start with the root directory or a drive letter.

def

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

Returns the parent directory of a path, if there is one.

If the path is that of the root directory or the root of a drive letter, none is returned. Otherwise, the path's parent directory is returned.

def

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

Splits a path into a list of individual file names at the platform-specific path separator.

def

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

Extracts the last element of a path if it is a file or directory name.

Returns none if the last entry is a special name (such as . or ..) or if the path is the root directory.

def

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

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

If the filename contains multiple extensions, then only the last one is removed. Returns none if there is no file name at the end of the path.

Examples:

("app.exe" : System.FilePath).fileStem = some "app"
("file.tar.gz" : System.FilePath).fileStem = some "file.tar"
("files/" : System.FilePath).fileStem = none
("files/picture.jpg" : System.FilePath).fileStem = some "picture"

def

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

Extracts the extension part of p.fileName.

If the filename contains multiple extensions, then only the last one is extracted. Returns none if there is no file name at the end of the path.

Examples:

("app.exe" : System.FilePath).extension = some "exe"
("file.tar.gz" : System.FilePath).extension = some "gz"
("files/" : System.FilePath).extension = none
("files/picture.jpg" : System.FilePath).extension = some "jpg"

def

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

Appends the extension ext to a path p.

ext should not have 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
System.FilePath.withExtension
  (p : System.FilePath) (ext : String) :
  System.FilePath

Replaces the current extension in a path p with ext, adding it if there is no extension. If the path has multiple file extensions, only the last one is replaced. If the path has no filename, or if ext is the empty string, then the filename is returned unmodified.

ext should not have a leading ., as this function adds one.

Examples:

("files/picture.jpeg" : System.FilePath).withExtension "jpg" = ⟨"files/picture.jpg"⟩
("files/" : System.FilePath).withExtension "zip" = ⟨"files/"⟩
("files" : System.FilePath).withExtension "zip" = ⟨"files.zip"⟩
("files/archive.tar.gz" : System.FilePath).withExtension "xz" = ⟨"files.tar.xz"⟩

def

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

Replaces the file name at the end of the path p with fname, placing fname in the parent directory of p.

If p has no parent directory, then fname is returned unmodified.

def

System.FilePath.pathSeparator : Char
System.FilePath.pathSeparator : Char

The character that separates directories.

On platforms that support multiple separators, System.FilePath.pathSeparator is the “ideal” one expected by users on the platform. System.FilePath.pathSeparators lists all supported separators.

def

System.FilePath.pathSeparators : List Char
System.FilePath.pathSeparators : List Char

The list of all path separator characters supported on the current platform.

On platforms that support multiple separators, System.FilePath.pathSeparator is the “ideal” one expected by users on the platform.

def

System.FilePath.extSeparator : Char
System.FilePath.extSeparator : Char

The character that separates file extensions from file names.

def

System.FilePath.exeExtension : String
System.FilePath.exeExtension : String

The file extension expected for executable binaries on the current platform, or "" if there is no such extension.

21.5.4. 与文件系统交互🔗

路径上的某些操作会参考文件系统。

structure

IO.FS.Metadata : Type
IO.FS.Metadata : Type

File metadata.

The metadata for a file can be accessed with System.FilePath.metadata/ System.FilePath.symlinkMetadata.

Constructor

IO.FS.Metadata.mk

Fields

accessed : IO.FS.SystemTime

File access time.

modified : IO.FS.SystemTime

File modification time.

byteSize : UInt64

The size of the file in bytes.

type : IO.FS.FileType

Whether the file is an ordinary file, a directory, a symbolic link, or some other kind of file.

numLinks : UInt64

The number of hard links to the file.

opaque

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

Returns metadata for the indicated file, following symlinks. Throws an exception if the file does not exist or the metadata cannot be accessed.

opaque

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

Returns metadata for the indicated file without following symlinks. Throws an exception if the file does not exist or the metadata cannot be accessed.

def

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

Checks whether the indicated path points to a file that exists. This function will traverse symlinks.

def

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

Checks whether the indicated path can be read and is a directory. This function will traverse symlinks.

structure

IO.FS.DirEntry : Type
IO.FS.DirEntry : Type

An entry in a directory on a filesystem.

Constructor

IO.FS.DirEntry.mk

Fields

root : System.FilePath

The directory in which the entry is found.

fileName : String

The name of the entry.

def

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

The path of the file indicated by the directory entry.

opaque

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

Returns the contents of the indicated directory. Throws an exception if the file does not exist or is not a directory.

def

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

Traverses a filesystem starting at the path p and exploring directories that satisfy enter, returning the paths visited.

The traversal is a preorder traversal, in which parent directories occur prior to any of their children. Symbolic links are followed.

structure

IO.AccessRight : Type
IO.AccessRight : Type

POSIX-style file permissions.

The FileRight structure describes these permissions for a file's owner, members of its designated group, and all others.

Constructor

IO.AccessRight.mk

Fields

read : Bool

The file can be read.

write : Bool

The file can be written to.

execution : Bool

The file can be executed.

def

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

Converts individual POSIX-style file permissions to their conventional three-bit representation.

This is the bitwise or of the following:

If the file can be read, 0x4, otherwise 0.
If the file can be written, 0x2, otherwise 0.
If the file can be executed, 0x1, otherwise 0.

Examples:

{read := true : AccessRight}.flags = 4
{read := true, write := true : AccessRight}.flags = 6
{read := true, execution := true : AccessRight}.flags = 5

structure

IO.FileRight : Type
IO.FileRight : Type

POSIX-style file permissions that describe access rights for a file's owner, members of its assigned group, and all others.

Constructor

IO.FileRight.mk

Fields

user : IO.AccessRight

The owner's permissions to access the file.

group : IO.AccessRight

The assigned group's permissions to access the file.

other : IO.AccessRight

The permissions that all others have to access the file.

def

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

Converts POSIX-style file permissions to their numeric representation, with three bits each for the owner's permissions, the group's permissions, and others' permissions.

def

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

Sets the POSIX-style permissions for a file.

opaque

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

Removes (deletes) a file from the filesystem.

To remove a directory, use IO.FS.removeDir or IO.FS.removeDirAll instead.

opaque

IO.FS.rename (old new : System.FilePath) : IO Unit
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.

opaque

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

Removes (deletes) a directory.

Removing a directory fails if the directory is not empty. Use IO.FS.removeDirAll to remove directories along with their contents.

def

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

Returns the contents of a UTF-8-encoded text file as an array of lines.

Newline markers are not included in the lines.

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

Creates a temporary file in the most secure manner possible and calls f with both a Handle to the already-opened file and its path. Afterwards, the temporary file is deleted.

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.

Use IO.FS.createTempFile to avoid the automatic deletion of the temporary file.

def

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

Creates a temporary directory in the most secure manner possible, providing its path to an IO action. Afterwards, all files in the temporary directory are recursively deleted, regardless of how or when they were created.

There are no race conditions in the directory’s creation. The directory is readable and writable only by the creating user ID. Use IO.FS.createTempDir to avoid the automatic deletion of the directory's contents.

opaque

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

Creates a directory at the specified path, creating all missing parents as directories.

def

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

Write the provided bytes to a binary file at the specified path.

def

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

Opens the file fn with the specified mode and passes the resulting file handle to f.

The file handle is closed when the last reference to it is dropped. If references escape f, then the file remains open even after IO.FS.withFile has finished.

opaque

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

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

opaque

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

Creates a temporary file in the most secure manner possible, returning both a Handle to the already-opened file and its path.

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.

It is the caller's job to remove the file after use. Use withTempFile to ensure that the temporary file is removed.

opaque

IO.FS.createTempDir : IO System.FilePath
IO.FS.createTempDir : IO System.FilePath

Creates a temporary directory in the most secure manner possible, returning the new directory's path. There are no race conditions in the directory’s creation. The directory is readable and writable only by the creating user ID.

It is the caller's job to remove the directory after use. Use withTempDir to ensure that the temporary directory is removed.

def

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

Reads the entire contents of the UTF-8-encoded file at the given path as a String.

An exception is thrown if the contents of the file are not valid UTF-8. This is in addition to exceptions that may always be thrown as a result of failing to read files.

opaque

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

Resolves a path to an absolute path that contains no '.', '..', or symbolic links.

This function coincides with the POSIX realpath function.

def

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

Write contents of a string to a file at the specified path using UTF-8 encoding.

def

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

Reads the entire contents of the binary file at the given path as an array of bytes.

opaque

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

Creates a directory at the specified path. The parent directory must already exist.

Throws an exception if the directory cannot be created.

21.5.5. 标准输入/输出🔗

在源自 Unix 或受 Unix 启发的操作系统上，standard input、standard output 和 standard error 是每个进程中可用的三个流的名称。通常，程序应从标准输入读取，将普通输出写入标准输出，并将错误消息写入标准错误。默认情况下，标准输入接收来自控制台的输入，而标准输出和标准错误输出到控制台，但这三者通常都重定向到管道或文件或从管道或文件重定向。

Lean 不是提供对操作系统标准 I/O 设施的直接访问，而是将它们包装在 Stream 中。此外，IO monad 包含对替换或本地覆盖它们的特殊支持。这种额外的间接级别使得可以在 Lean 程序中重定向输入和输出。

opaque

IO.getStdin : BaseIO IO.FS.Stream
IO.getStdin : BaseIO IO.FS.Stream

Returns the current thread's standard input stream.

Use IO.setStdin to replace the current thread's standard input stream.

Reading from Standard Input

在此示例中，IO.getStdin 和 IO.getStdout 分别用于获取当前标准输入和输出。这些可以读取和写入。

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

有了这个标准输入：

stdinLean user

标准输出是：

stdoutWho is it?Hello, Lean user

opaque

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

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

Use IO.getStdin to get the current standard input stream.

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 α
IO.withStdin.{u_1} {m : Type → Type u_1}
  {α : Type} [Monad m] [MonadFinally m]
  [MonadLiftT BaseIO m] (h : IO.FS.Stream)
  (x : m α) : m α

Runs an action with the specified stream h as standard input, restoring the original standard input stream afterwards.

opaque

IO.getStdout : BaseIO IO.FS.Stream
IO.getStdout : BaseIO IO.FS.Stream

Returns the current thread's standard output stream.

Use IO.setStdout to replace the current thread's standard output stream.

opaque

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

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

Use IO.getStdout to get the current standard output stream.

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 α
IO.withStdout.{u_1} {m : Type → Type u_1}
  {α : Type} [Monad m] [MonadFinally m]
  [MonadLiftT BaseIO m] (h : IO.FS.Stream)
  (x : m α) : m α

Runs an action with the specified stream h as standard output, restoring the original standard output stream afterwards.

opaque

IO.getStderr : BaseIO IO.FS.Stream
IO.getStderr : BaseIO IO.FS.Stream

Returns the current thread's standard error stream.

Use IO.setStderr to replace the current thread's standard error stream.

opaque

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

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

Use IO.getStderr to get the current standard error stream.

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 α
IO.withStderr.{u_1} {m : Type → Type u_1}
  {α : Type} [Monad m] [MonadFinally m]
  [MonadLiftT BaseIO m] (h : IO.FS.Stream)
  (x : m α) : m α

Runs an action with the specified stream h as standard error, restoring the original standard error stream afterwards.

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 × α)
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 × α)

Runs an action with stdin emptied and stdout and stderr captured into a String. If isolateStderr is false, only stdout is captured.

Redirecting Standard I/O to Strings

countdown 函数从指定数字开始倒计时，并将其进度写入标准输出。使用 IO.FS.withIsolatedStreams，可以将此输出重定向到字符串。

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

运行 countdown 会生成一个包含输出的字符串：

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

Live ↪

21.5.6. 文件和目录🔗

opaque

IO.currentDir : IO System.FilePath
IO.currentDir : IO System.FilePath

Returns the current working directory of the executing process.

opaque

IO.appPath : IO System.FilePath
IO.appPath : IO System.FilePath

Returns the file name of the currently-running executable.

def

IO.appDir : IO System.FilePath
IO.appDir : IO System.FilePath

Returns the directory that the current executable is located in.