feat: utilities for formatting tables

ImportGraph.lean

@@ -24,6 +24,7 @@ public import ImportGraph.Shake.EnvExtension
 public import ImportGraph.Shake.Environment
 public import ImportGraph.Shake.Workspace
 public import ImportGraph.Util.FindSorry
+public import ImportGraph.Util.TableMessage
 public import ImportGraph.WorkspaceModel.Base
 public import ImportGraph.WorkspaceModel.Build
 public import ImportGraph.WorkspaceModel.Model

ImportGraph/Util/TableMessage.lean

@@ -0,0 +1,73 @@
+/-
+Copyright (c) 2026 Thomas R. Murrills. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Thomas R. Murrills
+-/
+module
+
+
+import Lean.Elab.Command
+
+/-!
+# Formatting tables
+
+This module provides basic utilities for formatting tables with aligned columns.
+For now, we only supports tables of strings.
+
+## Future work
+
+- Specifying dividers and borders, padding characters, right/left alignment, column widths
+  - Ideally this is granular, e.g. per cell/row/column
+- Composing and stacking tables
+- Widget version using HTML tables to avoid awkward reflowing + allow `MessageData`
+-/
+
+namespace ImportGraph
+
+open ImportGraph
+
+public section
+
+/-- Pad a string on the right with `c : Char` (by default `' '`), until it reaches length `n`. Does
+not trim strings already over length `n` down to length `n`. -/
+@[inline] def String.rightPad (n : Nat) (s : String) (char : Char := ' ') :=
+  s.pushn char (n - s.positions.length)
+
+/-- Pad a string on the left with `c : Char` (by default `' '`), until it reaches length `n`. Does
+not trim strings already over length `n` down to length `n`. -/
+@[inline] def String.leftPad (n : Nat) (s : String) (char : Char := ' ') :=
+  "".pushn char (n - s.positions.length) ++ s
+
+namespace Table
+
+/-- A row with a fixed number of elements in a table such as `Array (Table.Row 5)`. (The `String`s
+in a `Row` are allowed to have any length.) -/
+protected abbrev Row (n : Nat) := Vector String n
+
+/-- Given an array of table rows, arranges them in a table. Each cell is left-aligned, and
+separated from the next cell in the row by a space. Spaces at the end of each row are trimmed. -/
+protected def formatSimple (rows : Array (Table.Row n)) : String := Id.run do
+  if h : rows.size > 0 then
+    let mut colWidths := rows[0].map (·.positions.length)
+    for h : i in 1...rows.size do
+      colWidths := colWidths.zipWith (max · ·.positions.length) rows[i]
+    let mut table := ""
+    for hRow : rowIdx in 0...rows.size do
+      for hCol : i in 0...n do
+        if h : i + 1 < n then
+          table := table ++ rows[rowIdx][i].rightPad colWidths[i] |>.push ' '
+        else
+          -- The last column needs neither padding nor a `' '` separator
+          -- However, it may still have spaces (e.g. empty cell) so trim them; do not drop `'\n'`.
+          table := table ++ rows[rowIdx][i] |>.dropEndWhile (· = ' ') |>.copy
+      unless rowIdx + 1 == rows.size do
+        table := table.push '\n'
+    return table
+  else return ""
+
+/-- An empty row in a table. -/
+def emptyRow {n} : Table.Row n := Vector.replicate n ""
+
+/-- Increase the size of a row by padding it on the right with empty cells. -/
+def Row.rightPad (row : Table.Row n) (h : n ≤ m := by grind) : Table.Row m :=
+  (show max m n = m by grind) ▸ row.rightpad m ""

ImportGraphTest.lean

@@ -22,6 +22,7 @@ import ImportGraphTest.NormImports
 import ImportGraphTest.NoLakeAxioms
 import ImportGraphTest.Shake.Algebra
 import ImportGraphTest.Shake.Workspace
+import ImportGraphTest.TableMessage
 import ImportGraphTest.ToTarget
 import ImportGraphTest.Unused
 import ImportGraphTest.Used

ImportGraphTest/Shake/Algebra.lean

@@ -7,6 +7,7 @@ module
 
 public meta import ImportGraph.Shake.Algebra
 public meta import Lean.Elab.Command
+public meta import ImportGraph.Util.TableMessage
 
 /-!
 # Tests for the import hierarchy algebra
@@ -35,26 +36,26 @@ def NeedsKind.allPairs : Array (NeedsKind × NeedsKind) :=
 def pad (n : Nat) (s : String) : String := s ++ "".pushn ' ' (n - s.length)
 
 /-- The composition table of `NeedsKind.andThen`, with the first factor on the left. -/
-meta def compositionTable : String :=
-  let row (cells : List String) := (String.join <| cells.map (pad 7)).trimAsciiEnd.toString
+meta def compositionTable : String := Id.run do
   -- push meta to the end instead of `all` for a cleaner table
-  let ks := NeedsKind.all.insertionSort (!·.isMeta && ·.isMeta) |>.toList
-  "\n".intercalate <|
-    row ("(↓) ≫ (→) " :: ks.map shortName) ::
-      ks.map fun k₁ =>
-        row <| pad 10 (shortName k₁) :: ks.map fun k₂ =>
-          if h : k₁.target = k₂.source then shortName (andThen k₁ k₂) else "-"
+  let ks := NeedsKind.all.insertionSort (!·.isMeta && ·.isMeta)
+  let mut rows : Array (Table.Row (1 + ks.size)) :=
+    #[#v["(↓) ≫ (→)"] ++ ks.toVector.map shortName]
+  rows := rows ++ ks.map fun k₁ =>
+    #v[shortName k₁] ++ (ks.toVector.map fun k₂ =>
+      if h : k₁.target = k₂.source then shortName (k₁.andThen k₂) else "-")
+  Table.formatSimple rows
 
 /--
 info:
 
-(↓) ≫ (→) pub    priv   all    𝓶pub   𝓶priv  𝓶all
-pub       pub    priv   -      𝓶pub   𝓶priv  -
-priv      -      -      priv   -      -      𝓶priv
-all       -      -      all    -      -      𝓶all
-𝓶pub      𝓶pub   𝓶priv  -      𝓶pub   𝓶priv  -
-𝓶priv     -      -      𝓶priv  -      -      𝓶priv
-𝓶all      -      -      𝓶all   -      -      𝓶all
+(↓) ≫ (→) pub  priv  all   𝓶pub 𝓶priv 𝓶all
+pub       pub  priv  -     𝓶pub 𝓶priv -
+priv      -    -     priv  -    -     𝓶priv
+all       -    -     all   -    -     𝓶all
+𝓶pub      𝓶pub 𝓶priv -     𝓶pub 𝓶priv -
+𝓶priv     -    -     𝓶priv -    -     𝓶priv
+𝓶all      -    -     𝓶all  -    -     𝓶all
 -/
 #guard_msgs in
 #eval IO.println s!"\n\n{compositionTable}"
@@ -165,7 +166,7 @@ protected def Needs.randM (hierarchySize : Nat)
 
 -- TODO: should maybe choose randomly how many are in each "layer"?
 /-- A topologically sorted array of needs, i.e. one in which each `Needs` only refers to prior
-ones. If the config is `none`, it's randomized each time. This allows for more module-tomodule
+ones. If the config is `none`, it's randomized each time. This allows for more module-to-module
 variation in quality, perhaps more like a real repo. -/
 def Needs.randArrayM (hierarchySize : Nat)
     (cfg? : Option RandNeedsConfig := none) :

ImportGraphTest/TableMessage.lean

@@ -0,0 +1,33 @@
+module
+
+public meta import ImportGraph.Util.TableMessage
+
+import Lean.Elab.Command
+
+open ImportGraph
+
+/--
+info: Table:
+
+          header1 h2   header3!      h₄
+row₁:     item1   foo  bar           baz
+row₂:     item₂   foo₂ bar₂          baz₂
+
+row₃:     1       2    (long item 3) 4
+shortrow: a₁      a₂
+finalrow: 0       1    1             0
+-/
+#guard_msgs in
+run_cmd do
+  let mut rows : Array (Table.Row 5) := #[]
+  rows := rows.push #v["", "header1", "h2", "header3!", "h₄"]
+  let shortRow : Table.Row 3 := #v["shortrow:", "a₁", "a₂"]
+  rows := rows ++ #[
+    #v["row₁:", "item1", "foo", "bar", "baz"],
+    #v["row₂:", "item₂", "foo₂", "bar₂", "baz₂"],
+    Table.emptyRow,
+    #v["row₃:", "1", "2", "(long item 3)", "4"],
+    shortRow.rightPad,
+    #v["finalrow:", "0", "1", "1", "0"]
+  ]
+  Lean.logInfo m!"Table:\n\n{Table.formatSimple rows}"