Application: File Compression and Decompression🔗

Lean does not have built-in support for file compression, but we can easily call external programs like gzip or zip to perform these tasks.

Warning: Since we are using external programs, these are system-dependent and make sure to have the necessary tools installed on your system. Change the commands accordingly for different operating systems or compression formats.

Using the functions defined above, we can easily perform common system tasks like compressing files or creating archives.

Using gzip

The gzip command is a standard tool for single-file compression.

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

Creating a .zip Archive

To archive multiple files or directories, we can use the zip utility.

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

To decompress a .zip file, we can use the unzip command:

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

For any other compression formats, you can similarly call the appropriate command-line tool using the runExternalProgram function.