文件压缩与解压🔗

Lean 没有内置的文件压缩支持，但我们可以轻松调用像 gzip 或 zip 这样的外部程序来完成这些任务。关于如何从 Lean 运行外部命令的更多信息，参见派生子进程配方。

警告：由于我们使用的是外部程序，这些都依赖于系统，请确保你的系统上装有所需工具。对于不同的操作系统或压缩格式，请相应地更改命令。

利用上面定义的函数，我们可以轻松执行像压缩文件或创建归档这样的常见系统任务。

使用 gzip

gzip 命令是单文件压缩的标准工具。

def compressFile (path : System.FilePath) : IO Unit := do
  let _ ← runExternalProgram "gzip" #["-k", path.toString]
  IO.println s!"Compressed {path}"

创建 .zip 归档

要归档多个文件或目录，我们可以使用 zip 工具。

def createArchive (archiveName : String) 
    (files : Array String) : IO Unit := do
  let _ ← runExternalProgram "zip" (#[archiveName] ++ files)
  IO.println s!"Created archive {archiveName}"

要解压一个 .zip 文件，我们可以使用 unzip 命令：

def decompressArchive (archiveName : String) : IO Unit := do
  let _ ← runExternalProgram "unzip" #["-o", archiveName]
  IO.println s!"Decompressed archive {archiveName}"

对于任何其他压缩格式，你都可以类似地用 runExternalProgram 函数调用相应的命令行工具。