对已打开文件的引用。
文件句柄包装底层操作系统的文件描述符。没有显式关闭文件的操作：当文件句柄的最后一个引用被丢弃时， 文件会自动关闭。
句柄带有关联的读/写光标，用来决定在文件中的读写位置。
21.5. 文件、文件句柄与流
Lean 在所有受支持的平台上提供一致的文件系统 API。 其中的关键概念如下：
- 文件
文件是操作系统提供的一种抽象，它支持随机访问持久存储的数据；这些数据按目录组成层级结构。
- 目录
目录也称为文件夹，其中可以包含文件或其他目录。 从根本上说，目录把名称映射到其中包含的文件和／或目录。
- 文件句柄
文件句柄（
Handle）是对已打开以供读取和／或写入的文件的抽象引用。 文件句柄维护一种模式，用来确定是否允许读取和／或写入；它还维护一个指向文件中特定位置的游标。 通过文件句柄读取或写入都会推进该游标。 文件句柄可以是带缓冲的；这意味着通过文件句柄读取时，可能不会返回持久数据的当前内容，而写入时也可能不会立即修改这些内容。- 路径
文件主要通过路径（
System.FilePath）来访问。 路径是一个目录名序列，末尾也可能是文件名。 路径由字符串表示，其中的分隔符字符当前平台的分隔符字符列于System.FilePath.pathSeparators。用于分隔各个名称。路径的具体细节因平台而异。 绝对路径始于根目录；有些操作系统只有一个根目录，另一些则可能有多个根目录。 相对路径不以根目录开头，需要把另一个目录作为起点。 除普通目录外，路径还可以包含特殊目录名
.和..：前者指其所在目录，后者指路径中的上一级目录。文件名乃至路径可以以一个或多个标识文件类型的扩展名结尾。 扩展名由字符
System.FilePath.extSeparator分隔。 在某些平台上，可执行文件具有特殊扩展名（System.FilePath.exeExtension）。- 流
流是文件之上的高层抽象，既提供额外功能，也隐藏文件的一些细节。 文件句柄本质上只是对操作系统表示的薄封装，而流则在 Lean 中实现为名为
IO.FS.Stream的结构。 由于流在 Lean 中实现，用户代码可以创建额外的流，并与标准库提供的流无缝配合使用。
21.5.1. 底层文件 API
在最底层，文件通过 Handle.mk 显式打开。
当句柄对象的最后一个引用被丢弃时，文件随即关闭。
除了确保文件句柄不再有任何引用外，没有其他显式关闭句柄的方法。
不透明定义
以给定 mode 打开位于 fn 的文件。
如果文件无法打开，则会抛出异常。
归纳类型
文件应以读取、写入、创建并写入，或追加的哪种方式打开。
在操作系统层面，这会转换为文件句柄的模式（即一组 open 标志以及一个 fdopen 模式）。
此数据类型表示的所有模式都不会转换行结束符（即 Windows 上的 O_BINARY）。此外，这些模式不会在进程创建时被继承（即 Windows 上的 O_NOINHERIT，以及其他平台上的 O_CLOEXEC）。
操作系统特有信息：
构造子
IO.FS.Mode.write : IO.FS.Mode
文件应以写入方式打开。
如果文件已存在，则会被截断为零长度。否则会创建一个新文件。读/写光标会定位到文件开头。
-
open标志：O_WRONLY | O_CREAT | O_TRUNC -
fdopen模式：w
IO.FS.Mode.writeNew : IO.FS.Mode
应创建一个新文件以供写入。
如果文件已经存在，则会报错。会创建一个新文件，并将读/写光标定位到开头。
-
open标志：O_WRONLY | O_CREAT | O_TRUNC | O_EXCL -
fdopen模式：w
IO.FS.Mode.append : IO.FS.Mode
文件应以写入方式打开。
如果文件尚不存在，则会创建它。如果文件已存在，则会打开它，并将读/写光标定位到文件末尾。
-
open标志：O_WRONLY | O_CREAT | O_APPEND -
fdopen模式：a
不透明定义
从该句柄中最多读取给定数量的字节。如果返回的数组为空，则表示已到达文件结束标记（EOF）。
遇到 EOF 并不会关闭句柄。后续读取仍可能阻塞并返回更多数据。
定义
将文件句柄中剩余的全部内容读取为 UTF-8 编码字符串。如果内容不是有效的 UTF-8，则会抛出异常。
底层文件不会自动关闭，后续从该句柄读取仍可能阻塞和/或返回数据。
定义
读取文件句柄中剩余的全部内容，直到遇到文件结束标记（EOF）。
遇到 EOF 时底层文件不会自动关闭，后续从该句柄读取仍可能阻塞和/或返回数据。
定义
读取文件句柄中剩余的全部内容，直到遇到文件结束标记（EOF）。
遇到 EOF 时底层文件不会自动关闭，后续从该句柄读取仍可能阻塞和/或返回数据。
不透明定义
从该句柄读取 UTF-8 编码文本，直到并包括下一个换行符。如果返回的字符串为空，则表示已到达文件结束标记（EOF）。
遇到 EOF 并不会关闭句柄。后续读取仍可能阻塞并返回更多数据。
定义
将字符串内容写入该句柄，并在其后附加一个换行符。使用 UTF-8。
不透明定义
刷新与该句柄关联的输出缓冲区，将任何尚未写出的数据写入关联输出设备。
不透明定义
将读/写光标回绕到该句柄所对应文件的开头。
不透明定义
将该句柄截断到其当前读/写光标位置。
此操作不会自动刷新输出缓冲区，因此输出设备的内容可能不会立刻反映这项变化。这通常不会导致问题，因为读/写光标会计入缓冲写入。然而，若先进行缓冲写入，再执行 IO.FS.Handle.rewind，然后执行 IO.FS.Handle.truncate，最后关闭文件，则可能产生一个非空文件。若不确定，请在截断前调用 IO.FS.Handle.flush。
不透明定义
获取该句柄上的排它锁或共享锁。如有必要，会阻塞等待锁可用。
当已经持有共享锁时，再获取排它锁 并不能 可靠地成功：这在类 Unix 系统上可行，但在 Windows 上不行。
不透明定义
不透明定义
释放此前在该句柄上获取的任何锁。即使此前没有获取锁，也会成功。
一个文件，多个句柄
该程序持有同一文件的两个句柄。
由于每个句柄的文件 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!B21.5.2. 流
结构体
POSIX 流的纯 Lean 抽象。这些流既可以表示底层 POSIX 流，也可以由 Lean 代码实现。
由于标准输入、标准输出和标准错误都是可被覆盖的 IO.FS.Stream，Lean 代码可以捕获并重定向输入与输出。
构造子
IO.FS.Stream.mk
字段
flush : IO Unit
刷新该流的输出缓冲区。
read : USize → IO ByteArray
从该流中最多读取给定数量的字节。
如果返回的数组为空，则表示已到达文件结束标记（EOF）。EOF 实际上不会关闭流，因此后续读取仍可能阻塞并返回更多数据。
write : ByteArray → IO Unit
将给定字节写入该流。
如果该流表示磁盘文件等物理输出设备，则结果可能会被缓冲。调用 FS.Stream.flush 以同步其内容。
getLine : IO String
从该流读取文本，直到并包括下一个换行符。
如果返回的字符串为空，则表示已到达文件结束标记（EOF）。EOF 实际上不会关闭流，因此后续读取仍可能阻塞并返回更多数据。
putStr : String → IO Unit
将给定字符串写入该流。
isTty : BaseIO Bool
如果该流引用的是 Windows 控制台或 Unix 终端，则返回 true。
定义
从对某个缓冲区的可变引用创建一个流。
所得流会模拟一个文件：写入时修改该引用的内容，读取时从其中读取。这些流可与 IO.withStdin、
IO.setStdin 以及标准输出和标准错误的对应操作符一起使用，以重定向输入和输出。
定义
从文件句柄创建一个 Lean 流。该流的每个操作都由对应的文件句柄操作实现。
定义
将字符串内容写入该流，并在其后附加一个换行符。
21.5.3. 路径
路径由字符串表示。
不同平台采用不同的路径约定：有些使用斜杠（/）作为目录分隔符，另一些使用反斜杠（\）。
有些平台区分大小写，另一些则不区分。
文件名可能采用不同的 Unicode 编码与规范化形式表示；有些平台还把文件名视为字节序列而非字符串。
在一个系统上表示绝对路径的字符串，在另一个系统上甚至可能不是有效路径。
为了编写尽可能兼容多个系统的 Lean 代码，最好使用 Lean 的路径操作原语，而不是直接操作字符串。
System.FilePath.join 等辅助函数会考虑平台特有的绝对路径规则；System.FilePath.pathSeparator 包含当前平台适用的路径分隔符；System.FilePath.exeExtension 则包含可执行文件所需的扩展名。
请勿硬编码这些规则。
FilePath 具有 Div 类型类的实例，因此可以使用斜杠运算符拼接路径。
结构体
文件系统中的一条路径。
路径由一系列目录以及最后的文件名或目录名组成。它们由平台相关的分隔字符分隔（见 System.FilePath.pathSeparator）。
字段
toString : String
路径的字符串表示。
定义
通过在文件名列表之间插入当前平台的路径分隔符，从而构造一条路径。
定义
拼接两条路径，并考虑绝对路径的情况。此操作也可通过 / 运算符访问。
如果 sub 是绝对路径，则会丢弃 p 并返回 sub。如果 sub 是相对路径，则会用平台特定的路径分隔符将其附加到 p 上。
定义
规范化一条路径，返回一条与之等价、但可能更符合平台约定的路径。
特别地：
-
在 Windows 上，驱动器盘符会被转成大写。
-
在支持多种路径分隔符的平台上（也就是
System.FilePath.pathSeparators的长度大于一时），替代分隔符会被替换为首选路径分隔符。
无法保证两条等价路径规范化后一定得到同一条路径。
定义
绝对路径从根目录或驱动器盘符开始。通过绝对路径访问文件不依赖于当前工作目录。
定义
相对路径是指其解释依赖当前工作目录的路径。相对路径不会以根目录或驱动器盘符开头。
定义
在平台特定的路径分隔符处，将路径拆分为单个文件名的列表。
定义
提取 p.fileName 的主干（不含扩展名的部分）。
如果文件名包含多个扩展名，则只移除最后一个。如果路径末尾没有文件名，则返回 none。
示例：
-
("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"
定义
提取 p.fileName 的扩展名部分。
如果文件名包含多个扩展名，则只提取最后一个。如果路径末尾没有文件名，则返回 none。
示例：
-
("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"
定义
将扩展名 ext 追加到路径 p。
ext 不应带前导 .，因为此函数会自行添加。如果 ext 为空字符串，则不会添加 .。
与 System.FilePath.withExtension 不同，此函数不会移除任何已有扩展名。
定义
将路径 p 当前的扩展名替换为 ext；如果没有扩展名，则添加它。若路径包含多个文件扩展名，则只替换最后一个。若路径没有文件名，或者 ext 为空字符串，则原样返回该文件名。
ext 不应带前导 .，因为此函数会自行添加。
示例：
-
("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"⟩
定义
将路径 p 末尾的文件名替换为 fname，并将 fname 放入 p 的父目录中。
如果 p 没有父目录，则原样返回 fname。
定义
分隔目录的字符。
在支持多种分隔符的平台上，System.FilePath.pathSeparator 是该平台用户期望的“理想”分隔符。System.FilePath.pathSeparators 列出了所有受支持的分隔符。
定义
当前平台上可执行二进制文件应使用的文件扩展名；若不存在此类扩展名，则为 ""。
21.5.4. 与文件系统交互
有些路径操作会查询文件系统。
不透明定义
返回指定文件的元数据，并跟随符号链接。若文件不存在或无法访问元数据，则抛出异常。
不透明定义
返回指定文件的元数据，但不跟随符号链接。若文件不存在或无法访问元数据，则抛出异常。
定义
检查指定路径是否指向一个存在的文件。此函数会跟随符号链接。
定义
检查指定路径是否可读取且为目录。此函数会跟随符号链接。
结构体
文件系统中某个目录内的一个条目。
定义
该目录项所指示文件的路径。
不透明定义
返回指定目录的内容。若文件不存在或不是目录，则抛出异常。
定义
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)
从路径 p 开始遍历文件系统，并探索满足 enter 的目录，返回访问到的路径。
此遍历是前序遍历，即父目录会先于其任何子项出现。符号链接会被跟随。
结构体
POSIX 风格的文件权限。
FileRight 结构为文件所有者、其指定组成员以及其他所有人描述这些权限。
定义
将各个 POSIX 风格文件权限转换为其传统的三位表示。
它是以下各项按位 or 的结果：
-
如果文件可读，则为
0x4，否则为0。 -
如果文件可写，则为
0x2，否则为0。 -
如果文件可执行，则为
0x1，否则为0。
示例：
-
{read := true : AccessRight}.flags = 4 -
{read := true, write := true : AccessRight}.flags = 6 -
{read := true, execution := true : AccessRight}.flags = 5
结构体
POSIX 风格的文件权限，描述文件所有者、文件所属组的成员以及其他所有人的访问权。
构造子
IO.FileRight.mk
字段
user : IO.AccessRight
文件所有者的文件访问权限。
group : IO.AccessRight
文件所属组的文件访问权限。
other : IO.AccessRight
其他所有人的文件访问权限。
定义
将 POSIX 风格的文件权限转换为数值表示；所有者权限、用户组权限和其他用户权限各占三位。
定义
设置文件的 POSIX 风格权限。
不透明定义
将文件或目录 old 移动到新位置 new。
定义
以行数组的形式返回 UTF-8 编码文本文件的内容。
返回的各行不包含换行标记。
定义
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 α
以尽可能安全的方式创建临时文件，并将已打开文件的 Handle 及其路径一并传给 f。调用结束后会删除该临时文件。
文件的创建过程不存在竞态条件。只有创建该文件的用户 ID 能读写它；此外，在 UNIX 风格的平台上，任何人都不能执行该文件。
若不希望自动删除临时文件，请使用 IO.FS.createTempFile。
定义
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 α
以尽可能安全的方式创建临时目录，并将其路径提供给一个 IO 操作。调用结束后，无论目录中的文件以何种方式或在何时创建，都会递归删除所有文件。
目录的创建过程不存在竞态条件。只有创建该目录的用户 ID 能读写它。若不希望自动删除目录内容，请使用 IO.FS.createTempDir。
不透明定义
在指定路径创建目录，并把所有缺失的父路径一并创建为目录。
定义
将所提供的字节写入指定路径的二进制文件。
定义
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 α
以指定的 mode 打开文件 fn，并将得到的文件句柄传给 f。
文件句柄的最后一个引用被丢弃时，句柄才会关闭。如果有引用逃逸出 f，那么即使 IO.FS.withFile 已执行完毕，文件也仍保持打开。
不透明定义
以未指定的顺序删除给定目录中包含的所有文件与目录，从而彻底移除该目录。符号链接会被删除，但不会被跟随。如果任何所含条目无法删除，或在执行期间又有条目新建，则操作失败。
不透明定义
以尽可能安全的方式创建临时文件，并返回已打开文件的 Handle 及其路径。
文件的创建过程不存在竞态条件。只有创建该文件的用户 ID 能读写它；此外，在 UNIX 风格的平台上，任何人都不能执行该文件。
调用方负责在使用后移除该文件。要确保临时文件被移除，请使用 withTempFile。
不透明定义
以尽可能安全的方式创建临时目录，并返回新目录的路径。目录的创建过程不存在竞态条件。只有创建该目录的用户 ID 能读写它。
调用方负责在使用后移除该目录。要确保临时目录被移除，请使用 withTempDir。
定义
使用 UTF-8 编码将字符串内容写入指定路径的文件。
定义
将给定路径下二进制文件的全部内容读取为字节数组。
不透明定义
在指定路径创建目录。父目录必须已经存在。
如果无法创建目录，则抛出异常。
21.5.5. 标准 I/O
在源自 Unix 或受其启发的操作系统中，标准输入、标准输出和标准错误是每个进程中可用的三个流的名称。 通常，程序应从标准输入读取数据，把普通输出写入标准输出，并把错误消息写入标准错误。 默认情况下，标准输入从控制台接收输入，而标准输出和标准错误向控制台输出；不过，这三个流经常被重定向到管道或文件，或从中读取。
Lean 并不直接提供对操作系统标准 I/O 设施的访问，而是用 Stream 对其加以封装。
此外，IO 单子还特别支持替换或局部覆盖这些流。
这一额外的间接层使 Lean 程序能够在内部重定向输入与输出。
从标准输入读取
本例分别使用 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
定义
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 α
以指定的流 h 作为标准输入运行一个操作，随后恢复原来的标准输入流。
定义
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 α
以指定的流 h 作为标准输出运行一个操作，随后恢复原来的标准输出流。
定义
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 α
以指定的流 h 作为标准错误运行一个操作，随后恢复原来的标准错误流。
定义
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 × α)
将标准 I/O 重定向到字符串
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
#eval runCountdown
运行 countdown 会得到一个包含输出的字符串：