feat: basic diffing utilities

ImportGraph.lean

@@ -23,7 +23,9 @@ public import ImportGraph.Shake.DeclNeeds
 public import ImportGraph.Shake.EnvExtension
 public import ImportGraph.Shake.Environment
 public import ImportGraph.Shake.Workspace
+public import ImportGraph.Util.Diff
 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/Shake/Basic.lean

@@ -301,6 +301,9 @@ Rephrasing of `f (n.get k)` for readability. -/
 @[inline] def foldWithKind (n : Needs) (f : α → NeedsKind → Bitset → α) (init : α) : α :=
   NeedsKind.all.foldl (init := init) fun a k => n.applyAt k (f a k)
 
+/-- The union of all bitsets in a `Needs`-/
+def flatten (n : Needs) : Bitset := n.fold (· ∪ ·) (init := ∅)
+
 /-- Applies `f` to all component `Bitset`s of the given `Needs`. -/
 @[specialize f] def map (n : Needs) (f : Bitset → Bitset) : Needs where
   pub      := f n.pub
@@ -429,6 +432,17 @@ instance : ToString NeedsKind where
     | .privOfPriv     => "all"
     | .metaPrivOfPriv => "meta all"
 
+/-- The prefix to the import command corresponding to the import. If `clarifyPriv` is `true`,
+(default `false`), we include "`private`" in front of private imports. This is useful in display
+situations, even though it is not a valid form of `import`. -/
+def toImportString (clarifyPriv := false) : NeedsKind → String
+  | .pub      => "public import"
+  | .metaPub  => "public meta import"
+  | .priv     => s!"{if clarifyPriv then "private " else ""}import"
+  | .metaPriv => s!"{if clarifyPriv then "private " else ""}meta import"
+  | .privOfPriv     => "import all"
+  | .metaPrivOfPriv => "meta import all"
+
 /-- The `NeedsKind`s which land (directly) in the private scope. -/
 @[inline, expose, grind] def toPrivate   : Array NeedsKind :=
   #[.priv, .privOfPriv, .metaPriv, .metaPrivOfPriv]
@@ -530,4 +544,16 @@ def connecting? (src tgt : Environment.Visibility) (isMeta : Bool := false) : Op
   | .private, .private => some { isExported := false, isMeta, isAll := true }
   | .private, .public  => none
 
-end ImportGraph.Shake.NeedsKind
+end NeedsKind
+
+namespace Provides
+
+/-- Intersects each field of two `Provides`.
+
+Generally, intersection is not meaningful on a bare `Needs`, but is meaningful on a
+transitively closed and linearized `Provides`.
+
+We avoid making this an instance of `Inter` to avoid `a ∩ b` succeeding on `Needs`. -/
+@[inline] def inter (a b : Provides) := a.map₂ b (· ∩ ·)
+
+end Provides

ImportGraph/Util/Diff.lean

@@ -0,0 +1,5 @@
+module
+
+public import ImportGraph.Util.Diff.Basic
+public import ImportGraph.Util.Diff.Message
+public import ImportGraph.Util.Diff.Shake

ImportGraph/Util/Diff/Basic.lean

@@ -0,0 +1,167 @@
+/-
+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
+
+public section
+
+open Lean
+
+namespace ImportGraph
+
+namespace Diff
+
+protected class Measurable α where
+  measure : α → Nat
+export Measurable (measure)
+
+instance : Diff.Measurable Nat := ⟨id⟩
+
+open Diff
+
+/-- If an integer is (strictly) greater than 0, display it with `+`. -/
+def Int.toStringWithSign (i : Int) := if i > 0 then s!"+{i}" else s!"{i}"
+
+/-- A simple structure with two states, `initial : α` and `final : α`, which models a transition. -/
+structure Transition (α : Type u) where
+  /-- The state before `final`. -/
+  initial : α
+  /-- The state after `initial`. -/
+  final : α
+deriving Inhabited, Hashable, BEq, Repr
+
+namespace Transition
+
+/-- Apply `f` to both the initial and final state. -/
+@[inline] def map (t : Transition α) (f : α → β) : Transition β where
+  initial := f t.initial
+  final := f t.final
+
+/-- The difference between the measures of the `final` state and `initial` state. -/
+@[inline] def delta (t : Transition α) [Diff.Measurable α] : Int :=
+  (measure t.final : Int) - measure t.initial
+
+/-- `abbrev` for `Transition Nat`. The result of measuring a `Transition` with
+`Transition.measure`. -/
+protected abbrev Measured := Transition Nat
+
+@[inline] def measure (t : Transition α) [Diff.Measurable α] : Transition.Measured :=
+  t.map Diff.measure
+
+end Transition
+
+/-- A Venn diagram characterizing the changes between some (implicit, unspecified) initial and
+final state. -/
+structure Venn (α : Type u) where
+  /-- What the final state has gained that was not present in the initial state. -/
+  plus   : α
+  /-- What the initial state has lost that is no longer present in the final state. -/
+  minus  : α
+  /-- What the initial and final state have in common. -/
+  shared : α
+deriving Inhabited, Hashable, BEq, Repr
+
+/-- Convert a `Transition α` into a `Venn β` according to the provided notions of set difference
+and interesection. Note that this is slightly more general than using a `VennLike α` instance, as
+it allows changing the type to `β` and does not require `isEmpty`. -/
+@[inline] def Transition.toVennBy (t : Transition α) (sdiff : α → α → β) (inter : α → α → β) :
+    Venn β where
+  plus := sdiff t.final t.initial
+  minus := sdiff t.initial t.final
+  shared := inter t.initial t.final
+
+/-- Provides the structure necessary to view `α` as "setlike" enough to support `Venn`, namely a
+means of taking the set difference, a means of intersection, and a notion of emptiness. This
+typeclass is homogeneous, i.e. we assume that `α` itself is sufficient for representing both states
+and the differences/shared aspects between them. -/
+class VennLike α where
+  /-- A "set difference" such that `VennLike.sdiff a b` tells us what `a` has that `b` does not.  -/
+  protected sdiff : α → α → α
+  /--
+  An "intersection" such that `VennLike.inter a b` tells us what is common to both `a` and `b`.
+  -/
+  protected inter : α → α → α
+  /-- A notion of emptiness. `VennLike.isEmpty <| VennLike.sdiff a b = true` should imply that, for
+  the purposes of the Venn diagram, `a` is a "subset" of `b`. (Both directions should indicate
+  equality.) Likewise, `VennLike.isEmpty <| VennLike.inter a b` should imply that `a` is disjoint
+  from `b`. -/
+  protected isEmpty : α → Bool
+
+/-- Convert an `initial` and `final` state into their Venn diagram using the type's `VennLike`
+instance. -/
+def Transition.toVenn (t : Transition α) [VennLike α] : Venn α :=
+  t.toVennBy VennLike.sdiff VennLike.inter
+
+namespace Venn
+
+/-- Apply `f` to each field of `v`. -/
+@[inline] def map (v : Venn α) (f : α → β) : Venn β where
+  plus := f v.plus
+  minus := f v.minus
+  shared := f v.shared
+
+/-- A `v : Venn α` represents no change iff both `isEmpty v.plus` and `isEmpty v.minus`. -/
+@[inline] def isUnchangedBy (v : Venn α) (isEmpty : α → Bool) :=
+  isEmpty v.plus && isEmpty v.minus
+
+/-- A `v : Venn α` represents a change of some kind iff `v.plus` is not `isEmpty`  or\
+`v.minus` is not `isEmpty`. -/
+@[inline] def isChangedBy (v : Venn α) (isEmpty : α → Bool) := !(v.isUnchangedBy isEmpty)
+
+/-- If comparable, the relationship `final ≷ initial`, according to the provided notion of
+`isEmpty`.
+
+- `some .gt`: the `Venn` diagram implicitly represents a strict increase
+- `some .lt`: the `Venn` diagram implicitly represents a strict decrease
+- `some .eq`: no change in state at all
+- `none`: incomparable states (some increase, some decrease) -/
+@[inline] def compareBy? (v : Venn α) (isEmpty : α → Bool) : Option Ordering :=
+  match isEmpty v.plus, isEmpty v.minus with
+  | true,  true  => some .eq
+  | true,  false => some .lt
+  | false, true  => some .gt
+  | false, false => none
+
+/-- The net difference between the implicit initial and final state, collapsing the independent
+measurements of `plus` and `minus` together. -/
+@[inline] def delta (v : Venn α) [Diff.Measurable α] : Int :=
+  (Diff.measure v.plus : Int) - Diff.measure v.minus
+
+/-- A `v : VennMeasure` represents no change iff both `v.plus` and `v.minus` satisfy
+`VennLike.isEmpty`. -/
+@[inline] def isUnchanged (v : Venn α) [VennLike α] :=
+  v.isUnchangedBy VennLike.isEmpty
+
+/-- A `v : VennMeasure` represents a change of some kind iff either `v.plus` is not empty or
+`v.minus` is not empty, according to `VennLike.isEmpty`. -/
+@[inline] def isChanged (v : Venn α) [VennLike α] :=
+  !v.isUnchanged
+
+/-- If comparable, the relationship `final ≷ initial`.
+
+- `some .gt`: the `Venn` diagram implicitly represents a strict increase
+- `some .lt`: the `Venn` diagram implicitly represents a strict decrease
+- `some .eq`: no change in state at all
+- `none`: incomparable states (some increase, some decrease)
+
+The presence of a change is determined by `VennLike.isEmpty`. -/
+@[inline] def compare? (v : Venn α) [VennLike α] : Option Ordering :=
+  v.compareBy? VennLike.isEmpty
+
+/-- Apply `f` to the `shared` field. -/
+@[inline] def modifyShared (v : Venn α) (f : α → α) : Venn α := { v with shared := f v.shared }
+
+/-- Removes `ignored` from the `shared` field, according to `VennLike.sdiff`. This is useful when we want to ignore "obvious" common factors. -/
+def ignoreShared (ignored : α) (v : Venn α) [VennLike α] : Venn α :=
+  v.modifyShared (VennLike.sdiff · ignored)
+
+/-- Measurements of the parts of a Venn diagram comparing an (implicit, unspecified) initial state
+and final state. Abbrev for `Venn Nat`. -/
+protected abbrev Measured := Venn Nat
+
+@[inline] def measure (t : Venn α) [Diff.Measurable α] : Venn.Measured :=
+  t.map Diff.measure
+
+end Diff.Venn

ImportGraph/Util/Diff/Message.lean

@@ -0,0 +1,35 @@
+module
+
+public import ImportGraph.Util.Diff.Basic
+public import ImportGraph.Util.TableMessage
+
+public section
+
+namespace ImportGraph.Diff
+
+open ImportGraph.Diff
+
+namespace Transition
+
+/-- A header row for a table consisting of rows created by `Transition.toRow`. -/
+def header : Table.Row 4 := #v["", "Δ", "new", "old"]
+
+def toRow (rowHeader : String) (t : Transition α) [Diff.Measurable α] : Table.Row 4 :=
+  #v[rowHeader, t.delta.toStringWithSign, s!"{Diff.measure t.final}", s!"{Diff.measure t.initial}"]
+
+end Transition
+
+namespace Venn
+
+/-- A header row for a table consisting of rows created by `Venn.toRow`. -/
+def header : Table.Row 5 := #v["", "Δ", "+", "-", "∩"]
+
+/-- A row in a table for a single `VennMeasure` which follows the order in `VennMeasure.header`. -/
+def toRow (rowHeader : String) (t : Venn α) [Diff.Measurable α]: Table.Row 5 := #v[
+  rowHeader,
+  t.delta.toStringWithSign,
+  s!"+{Diff.measure t.plus}",
+  s!"-{Diff.measure t.minus}",
+  s!"{Diff.measure t.shared}"]
+
+end Venn

ImportGraph/Util/Diff/Shake.lean

@@ -0,0 +1,37 @@
+/-
+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
+
+public import ImportGraph.Util.Diff.Basic
+public import ImportGraph.Shake.Algebra
+
+public section
+
+namespace ImportGraph.Diff
+
+open ImportGraph Diff Shake
+
+instance : Diff.Measurable Bitset where
+  measure := (·.size)
+
+instance : VennLike Bitset where
+  sdiff := (· \ ·)
+  inter := (· ∩ ·)
+  isEmpty := (·.isEmpty)
+
+/-- Measures the Venn diagram of `Bitset`s at the given `NeedsKind`. -/
+def Venn.measureNeedsAt (k : NeedsKind) (needs : Venn Needs) : Venn.Measured :=
+  needs.map (·.get k |>.size)
+
+instance : Diff.Measurable Provides where
+  measure := (·.flatten.size)
+
+instance : VennLike Provides where
+  -- avoid linearizing to capture one `Provides` providing public while the other provides public
+  sdiff := (· \ ·)
+  -- `a` and `b` should be linearized already and remain linearized under intersection
+  inter := Provides.inter
+  isEmpty := (·.isEmpty)

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