Setting File Permissions🔗

Writing permissions for files is quite confusing since the API is not quite intuitive. Here is an example of how to set file permissions for a file path using the IO.AccessRight, IO.FileRight, and IO.setAccessRights APIs provided here in the Lean4 reference manual.

def setFilePermissions (path : System.FilePath) : 
    IO Unit := do
  -- Define specific access rights
  let rw : IO.AccessRight := 
    { read := true, write := true, execution := false } 
  let rOnly : IO.AccessRight := 
    { read := true, write := false, execution := false }

  -- Construct the FileRight structure
  -- Setting User to RW, Group to R, and Other to R
  let myRights : IO.FileRight := {
    user  := rw,
    group := rOnly,
    other := rOnly
  }

  -- Apply the rights to the file
  IO.setAccessRights path myRights
  IO.println s!"Access rights for {path} have been updated."