Append to a file

Stream: lean4

[Michael Rothgang]

The other day, I wanted to append a given string to a file. Would a method like the following be accepted?

/-- Append a given string at the end of an existing file. -/
def IO.FS.appendToFile (fname : FilePath) (content : String) : IO Unit := do
  let previous_content ← IO.FS.readFile fname
  IO.FS.writeFile fname (previous_content ++ content)

[Michael Rothgang]

(Obviously, this could have a better implemention which is less of a "polyfill". Also, I would like to document the edge cases of this method better: what happens if the file doesn't exist? If reading it fails? If writing the new content fails? Does this close the file afterwards?, etc. This detail is also missing from readFile, though - it's probably easiest to update both at the same time.)

[Alex J. Best]

You can open a file in append mode docs#IO.FS.Mode.append, I would think that that is better behaved

[Michael Rothgang]

Much nicer, thanks!