patches: lean4-0001 — refine Cycle.lean patch, standalone MonadCallStackFast, low-priority fallback instance

defects/lean4/patch/lean4-0001-lake-guardcycle-hashset.patch

@@ -11,9 +11,14 @@
 # Complexity gate:
 #   Linear chain N=1000: must complete in <1s (vs ~10s defective)
 #   k-scaling: time ratio for N=2k vs N=k must be <3x (O(N) not O(N²))
+#
+# Caller changes required (outside this file):
+#   Lake/Build/Topological.lean: add [Hashable κ] to recFetchAcyclic,
+#   recFetchMemoize. Both κ=BuildKey and κ=Name already derive/instance
+#   Hashable, so no new derivations needed at call sites.
 --- a/src/lake/Lake/Util/Cycle.lean
 +++ b/src/lake/Lake/Util/Cycle.lean
-@@ -1,87 +1,131 @@
+@@ -1,87 +1,136 @@
  /-
  Copyright (c) 2022 Mac Malone. All rights reserved.
  Released under Apache 2.0 license as described in the file LICENSE.
@@ -101,32 +106,37 @@
 -  else
 -    withCallStack (key :: parents) act
 +/--
-+Optional fast-path membership test for `guardCycle`.
++Optional fast-path membership test for monads that can answer stack-membership
++queries in better than O(N).
 +
-+Monads backed by a `HashSet` (e.g. `CycleT`) override `stackContains` to give
-+O(1) lookup. The default implementation falls back to `List.contains` — O(N) —
-+so every existing `MonadCycle` instance continues to compile without changes.
++Separate from `MonadCallStack` to avoid inheriting `getCallStack`/`withCallStack`
++fields, which would complicate diamond-inheritance for `CycleT`. `guardCycle`
++requires both `[MonadCycle κ m]` and `[MonadCallStackFast κ m]`.
 +
-+The `[Hashable κ]` constraint is required only by overriding instances. The
-+default implementation needs only `[BEq κ]` via `MonadCallStack`.
++The default instance below supplies an O(N) `List.contains` fallback so that
++all existing `MonadCycle` instances automatically satisfy this constraint
++without code changes.
 +-/
-+public class MonadCallStackFast (κ : outParam (Type u)) (m : Type u → Type v)
-+    extends MonadCallStack κ m where
++public class MonadCallStackFast (κ : outParam (Type u)) (m : Type u → Type v) where
 +  /-- Returns `true` iff `key` is already on the call stack. -/
-+  stackContains [BEq κ] (key : κ) : m Bool :=
-+    -- Default: O(N) List scan. Overridden by CycleT to O(1) HashSet lookup.
-+    return (← getCallStack).contains key
++  stackContains [BEq κ] (key : κ) : m Bool
 +
 +export MonadCallStackFast (stackContains)
 +
-+/-- Every `MonadCycle` instance automatically gets the O(N) fallback. -/
-+public instance (priority := low) [BEq κ] [MonadCycle κ m] : MonadCallStackFast κ m where
++/--
++Default instance: O(N) `List.contains` fallback.
++Every `MonadCycle` instance automatically satisfies `MonadCallStackFast`
++through this low-priority instance, so existing call sites need no changes
++beyond adding `[Hashable κ]` to `recFetchAcyclic` in Topological.lean.
++-/
++public instance (priority := low) [BEq κ] [Monad m] [MonadCycle κ m]
++    : MonadCallStackFast κ m where
 +  stackContains key := return (← getCallStack).contains key
 +
 +/--
 +`CycleT` carries `(Std.HashSet κ × List κ)` instead of a bare `List κ`.
 +
-+The `HashSet` enables O(1) membership tests in `guardCycle` — reducing a
++The `HashSet` enables O(1) membership tests in `guardCycle`, reducing a
 +linear-chain build traversal of N modules from O(N²) to O(N).
 +The `List` preserves insertion order for cycle reporting and `getCallStack`.
 +-/
@@ -136,9 +146,11 @@
 +/--
 +`MonadCycleOf` instance for `CycleT`.
 +
-+`getCallStack` returns the ordered `List κ` — backward compatible.
-+`withCallStack` accepts `List κ` (e.g. from `recFetchAcyclic`) and rebuilds
-+the `HashSet` once per push: O(N) per node, not O(N) per contains call.
++`getCallStack` returns the ordered `List κ` — backward compatible with all
++callers that consume `CallStack κ`.
++`withCallStack` accepts `List κ` (as supplied by `recFetchAcyclic`) and
++rebuilds the `HashSet` once per push: O(N) per node rather than O(N) per
++`contains` call.
 +-/
 +public instance [BEq κ] [Hashable κ] [Monad m] : MonadCycleOf κ (CycleT κ m) where
 +  throwCycle := throw
@@ -146,12 +158,15 @@
 +    let (_, list) ← read
 +    return list
 +  withCallStack stack x :=
-+    -- O(N) HashSet rebuild happens once when pushing a key onto the stack.
-+    -- guardCycle then pays O(1) for contains. Net: O(N) per node vs O(N²).
++    -- Rebuild HashSet from list: O(N) once per stack push.
++    -- guardCycle then pays O(1) for contains. Net: O(N) total, not O(N²).
 +    let hashSet := Std.HashSet.ofList stack
 +    x (hashSet, stack)
 +
-+/-- `CycleT` overrides `stackContains` to use the paired `HashSet` — O(1). -/
++/--
++`MonadCallStackFast` instance for `CycleT`: O(1) `HashSet` lookup,
++overriding the low-priority O(N) default.
++-/
 +public instance [BEq κ] [Hashable κ] [Monad m] : MonadCallStackFast κ (CycleT κ m) where
 +  stackContains key := do
 +    let (hashSet, _) ← read
@@ -161,16 +176,19 @@
 +Add `key` to the monad's `CallStack` before invoking `act`.
 +If adding `key` produces a cycle, the cyclic call stack is thrown.
 +
-+Requires `[MonadCallStackFast κ m]` for the membership test. All existing
-+`MonadCycle` instances automatically satisfy this via the low-priority default
-+instance (O(N) `List.contains` fallback). `CycleT`-backed monads satisfy it
-+with an O(1) `HashSet` lookup, fixing the O(N²) traversal defect.
++Uses `stackContains` for the membership test:
++  O(1) when `m` is `CycleT` (paired HashSet, added by this patch).
++  O(N) fallback for other `MonadCycle` instances (List.contains, original behavior).
++
++Note: callers must add `[Hashable κ]` to their own constraints. For Lake's
++primary callers this is already satisfied: `BuildKey` derives `Hashable`,
++`Name` has a built-in `Hashable` instance.
 +-/
 +@[inline] public def guardCycle
 +  [BEq κ] [Hashable κ] [Monad m] [MonadCycle κ m] [MonadCallStackFast κ m]
 +  (key : κ) (act : m α)
 +: m α := do
-+  -- O(1) for CycleT, O(N) fallback for other MonadCycle instances.
++  -- O(1) for CycleT; O(N) fallback for other MonadCycle instances.
 +  if ← stackContains key then
 +    let parents ← getCallStack
 +    throwCycle <| key :: (parents.partition (· != key)).1 ++ [key]