miscelleaneous

Random Lean experiments

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
/-
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)
      i := i + 1
    IO.println ""