How to Write JSONL files🔗

When writing JSONL, each object must be rendered as a single line without internal newlines. You can use Lean.Json.compress to ensure the output is compact.

Writing an array of JSON objects

def writeJsonlFile (path : System.FilePath)
  (data : Array Json) : IO Unit := do
  let lines := data.map (·.compress)
  IO.FS.writeFile path (String.intercalate "\n"
    lines.toList ++ "\n")

Writing custom structures to JSONL

For large logs or datasets, it is better to use a handle and write line by line.

structure LogEntry where
  timestamp : String
  level     : String
  message   : String
deriving ToJson

def writeLogs (path : System.FilePath)
    (logs : Array LogEntry) : IO Unit := do
  IO.FS.withFile path .write fun handle => do
    for log in logs do
      handle.putStrLn (toJson log).compress