Reading File Permissions🔗

To read the permissions of a file, Lean does not provide a built-in API for it(if you know one, please let us know!, I could not find one in the documentation). However, we can use the Linux stat command to get the permissions in octal format and then convert it to an IO.FileRight structure.

/-- Convert an octal digit to an IO.AccessRight structure. -/
def octalToAccessRight (c : Char) : IO.AccessRight :=
  let val := c.toString.toNat!
  { 
    read      := val / 4 % 2 == 1,
    write     := val / 2 % 2 == 1,
    execution := val % 2 == 1 
  }

/-- Reads the permissions of a file with `stat` command. -/
def getFilePermissions (path : System.FilePath) :
    IO IO.FileRight := do
  let out ← IO.Process.output {
    cmd  := "stat",
    args := #["-c", "%a", path.toString]
  }

  if out.exitCode != 0 
    then throw <| 
      IO.userError s!"Failed to run stat: {out.stderr}"

  -- The output is usually 3 digits
  let s := out.stdout.trimAscii.toString
  let chars := s.toList

  -- Handle cases with 3 digits (User, Group, Other)
  match chars with
  | [u, g, o] =>
      return {
        user  := octalToAccessRight u,
        group := octalToAccessRight g,
        other := octalToAccessRight o
      }
  | _ => throw <| 
      IO.userError s!"Unexpected permission format: {s}"

def demoPermissions (path : System.FilePath) : IO Unit := do
  -- Get current permissions
  let current ← getFilePermissions path
  IO.println s!"User can read: {current.user.read}"

  -- Modify permissions: Add execution for the user
  let updated := { current with 
    user := { current.user with execution := true },
    group := { current.group with write := true },
    other := { current.other with execution := true },
  }
  
  -- Apply updated permissions
  IO.setAccessRights path updated
  IO.println "Updated user to allow execution."

This works nicely on Unix systems, you can modify the commands accordingly. Note that when you are setting permissions, you will only change the permissions mentioned in the IO.FileRight structure, previously set permissions that are not mentioned will remain unchanged.