Clean up code for plotting scripts

Changes

2 changed files (+15/-18)

• CommitGraph.lean
  • @@ -62,13 +62,5 @@ def main : IO Unit := do
    IO.print s!"{date} " date := date.addDays 7 IO.print <| colors[if cnt = 0 then 0 else if cnt < m / 8 then 1 else if cnt < m / 4 then 2 else if cnt < m / 2 then 3 else 4]'(by grind) - -- IO.print <| colors[if cnt = 0 then 0 else 4 * (cnt - 1) / m + 1]'(by - -- by_cases h : cnt = 0 - -- · grind - -- · simp [h] - -- have : cnt ≤ m := List.le_max?_getD_of_mem (by grind) - -- suffices 4 * (cnt - 1) / m < 4 by grind - -- apply Nat.div_lt_iff_lt_mul (by grind) |>.mpr - -- grind) i := i + 1 IO.println ""
• Plot.lean
  • @@ -1,8 +1,7 @@
    import Std.Time open Std.Time - def csv_filename := do - return (← IO.currentDir) / "log.csv" + def csv_filename := "log.csv" def parse_csv filename (parse_row : List String → Option α) := do return (← IO.FS.readFile filename).splitOn "\n" |>.toArray |>.map (λ (l : String) ↦
  • @@ -15,7 +14,7 @@ instance : LT (DateTime TimeZone.UTC) := ltOfOrd
    instance : LE PlainDate := leOfOrd def main := do - let lines ← parse_csv (← csv_filename) λ l ↦ match l with + let lines ← parse_csv csv_filename λ l ↦ match l with | [a, b, c] => match ZonedDateTime.fromISO8601String b with | .ok b => some (b.toDateTime.convertTimeZone TimeZone.UTC, ZonedDateTime.fromISO8601String c
  • @@ -51,13 +50,19 @@ def main := do
    let m := daily.toList.max?.getD 0 let colors := [" ", "░", "▒", "▓", "█"] i := 0 + date := start_date for h : cnt in daily do if i % 7 = 0 then - IO.print s!"{start_date.addDays <| Day.Offset.ofNat i} " - IO.print (colors[5 * cnt / (m + 1)]'(by - have : cnt ≤ m := List.le_max?_getD_of_mem (by grind) - apply Nat.div_lt_iff_lt_mul (by grind) |>.mpr - grind)) + if i > 0 then IO.println "" + IO.print s!"{date} " + date := date.addDays 7 + IO.print <| colors[if cnt = 0 then 0 else 4 * (cnt - 1) / m + 1]'(by + by_cases h : cnt = 0 + · grind + · simp [h] + have : cnt ≤ m := List.le_max?_getD_of_mem (by grind) + suffices 4 * (cnt - 1) / m < 4 by grind + apply Nat.div_lt_iff_lt_mul (by grind) |>.mpr + grind) i := i + 1 - if i % 7 = 0 then - IO.println "" + IO.println ""