String.splitOn is getting deprecated soon https://github.com/leanprover/lean4/pull/11250

Changes

3 changed files (+11/-5)

• CommitGraph.lean
  • @@ -38,7 +38,7 @@ instance : LE PlainDate := leOfOrd
    def main : IO Unit := do let stdin ← IO.getStdin - let lines := (← stdin.readToEnd).splitOn "\n" |>.toArray |>.filterMap fun x ↦ + let lines := (← stdin.readToEnd).split "\n" |>.toArray |>.filterMap fun x ↦ (Timestamp.toPlainDateAssumingUTC ∘ Timestamp.ofSecondsSinceUnixEpoch ∘ Second.Offset.ofNat) <$> x.toNat? let sorted_lines := lines.qsortOrd if h : 0 < sorted_lines.size then
• Compose.lean
  • @@ -5,7 +5,11 @@ def ofHex a b := let f (x : Char) := x.toNat - (if x.toNat ≤ '9'.toNat then '0
    16 * (f a) + (f b) |> Char.ofNat def main := do - let keysym := (← IO.FS.readFile "keysymdef.h").splitOn "\n" |>.map (fun l : String ↦ (ofHex (String.Pos.Raw.get! l ⟨45⟩) (String.Pos.Raw.get! l ⟨46⟩), Substring.Raw.mk l ⟨11⟩ ⟨30⟩ |>.takeWhile (· ≠ ' ') |>.toString)) |> Std.HashMap.ofList + let keysym := (← IO.FS.readFile "keysymdef.h").split "\n" + |>.toStringList + |>.map (fun l : String ↦ (ofHex (String.Pos.Raw.get! l ⟨45⟩) (String.Pos.Raw.get! l ⟨46⟩), Substring.Raw.mk l ⟨11⟩ ⟨30⟩ + |>.takeWhile (· ≠ ' ') |>.toString)) + |> Std.HashMap.ofList IO.println "# Generated by https://git.unnamed.website/miscelleaneous/tree/Compose.lean" IO.println "include \"%L\"" let raw_abbrs ← IO.Process.run { cmd := "curl", args := #["https://raw.githubusercontent.com/vasnesterov/vscode-lean4/refs/heads/master/lean4-unicode-input/src/abbreviations.json"] }
• Plot.lean
  • @@ -2,11 +2,13 @@ import Std.Time
    open Std.Time def parse_csv filename (parse_row : List String → Option α) := do - return (← IO.FS.readFile filename).splitOn "\n" |>.toArray |>.map (fun (l : String) ↦ + return (← IO.FS.readFile filename).split "\n" |>.map (fun (l : String.Slice) ↦ l.replace "\\," "\n" - |>.splitOn "," - |>.map fun (s : String) ↦ s.replace "\n" ",") + |>.split "," + |>.toList + |>.map fun (s : String.Slice) ↦ s.replace "\n" ",") |>.filterMap parse_row + |>.toArray instance : LT (DateTime TimeZone.UTC) := ltOfOrd instance : LE PlainDate := leOfOrd