Random plotting tools

Changes

3 changed files (+141/-0)

• CommitGraph.lean (new)
  • @@ -0,0 +1,74 @@
    + /- + git log --format=%ct | lake exe commitgraph + + Sample output: + + 2025-04-20 ▒ ▓ + 2025-04-27 ▒ + 2025-05-04 ▓ ▓▒ + 2025-05-11 ▒▓ + 2025-05-18 ▒ █▓ + 2025-05-25 █▒ + 2025-06-01 + 2025-06-08 + 2025-06-15 + 2025-06-22 + 2025-06-29 ▒ + 2025-07-06 + 2025-07-13 ▓ + 2025-07-20 + 2025-07-27 ▒ + 2025-08-03 ▒ + 2025-08-10 ▓▓ ▓ + 2025-08-17 + 2025-08-24 ▓▓ █ + 2025-08-31 ▒ ▒▓▒▒▒ + 2025-09-07 ▒▒███ + 2025-09-14 ▒▒▒ + 2025-09-21 ▒ + 2025-09-28 ▒█ ▒ + 2025-10-05 ▓ ▓▓ + 2025-10-12 █▓ + -/ + + import Std.Time + open Std.Time + + instance : LE PlainDate := leOfOrd + + def main : IO Unit := do + let stdin ← IO.getStdin + let lines := (← stdin.readToEnd).splitOn "\n" |>.toArray |>.filterMap λ x ↦ + (Timestamp.toPlainDateAssumingUTC ∘ Timestamp.ofSecondsSinceUnixEpoch ∘ Second.Offset.ofNat) <$> x.toNat? + let sorted_lines := lines.qsortOrd + if h : 0 < sorted_lines.size then + let mut daily := #[] + let mut date := sorted_lines[0] + let mut i := 0 + while date ≤ sorted_lines[sorted_lines.size - 1] do + let mut cnt := 0 + while if h : i < sorted_lines.size then sorted_lines[i] = date else false do + cnt := cnt + 1 + i := i + 1 + daily := daily.push cnt + date := date.addDays 1 + let m := daily.toList.max?.getD 0 + let colors := [" ", "░", "▒", "▓", "█"] + i := 0 + date := sorted_lines[0] + for h : cnt in daily do + if i % 7 = 0 then + if i > 0 then IO.println "" + 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 (new)
  • @@ -0,0 +1,63 @@
    + import Std.Time + open Std.Time + + def csv_filename := do + return (← IO.currentDir) / "log.csv" + + def parse_csv filename (parse_row : List String → Option α) := do + return (← IO.FS.readFile filename).splitOn "\n" |>.toArray |>.map (λ (l : String) ↦ + l.replace "\\," "\n" + |>.splitOn "," + |>.map λ (s : String) ↦ s.replace "\n" ",") + |>.filterMap parse_row + + instance : LT (DateTime TimeZone.UTC) := ltOfOrd + instance : LE PlainDate := leOfOrd + + def main := do + 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 + |>.toOption.getD zoned("3000-01-01T00:00:00-00:00") + |>.toDateTime.convertTimeZone TimeZone.UTC) + | _ => none + | _ => none + -- Must be LT not LE! + let sorted_starts := lines.qsort λ x y ↦ x.1 < y.1 + let sorted_ends := lines.qsort λ x y ↦ x.2 < y.2 + IO.println <| sorted_ends.map Prod.snd + let start_date := date("2025-03-01") + let mut date := start_date + let cur_date ← Std.Time.PlainDate.now + let mut i := 0 + let mut j := 0 + let mut total := 0 + let mut log_size := 0 + let mut daily := #[] + while date ≤ cur_date do + while if h : i < sorted_starts.size then sorted_starts[i].1.toPlainDate ≤ date else false do + log_size := log_size + 1 + total := total + 1 + i := i + 1 + let mut cnt := 0 + while if h : j < sorted_ends.size then sorted_ends[j].2.toPlainDate ≤ date else false do + log_size := log_size - 1 + j := j + 1 + cnt := cnt + 1 + daily := daily.push cnt + IO.println s!"{date}{List.replicate (log_size / 2) " " |> "".intercalate}|{List.replicate ((total - log_size) / 2) " " |> "".intercalate}|" + date := date.addDays 1 + let m := daily.toList.max?.getD 0 + let colors := [" ", "░", "▒", "▓", "█"] + i := 0 + 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)) + i := i + 1 + if i % 7 = 0 then + IO.println ""
• lakefile.toml
  • @@ -15,6 +15,10 @@ root = "Main"
    name = "gcd" root = "Gcd" + [[lean_exe]] + name = "commitgraph" + root = "CommitGraph" + [[require]] name = "mathlib" scope = "leanprover-community"