diff --git a/defects/lean4/patch/lean4-0001-lake-guardcycle-hashset.patch b/defects/lean4/patch/lean4-0001-lake-guardcycle-hashset.patch index d8f0d2748..7db413486 100644 --- a/defects/lean4/patch/lean4-0001-lake-guardcycle-hashset.patch +++ b/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]