From 0c61e26bf68ab56ec37578ec82f7abb519ee6da9 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Tue, 29 Oct 2024 00:40:26 +1100 Subject: [PATCH] . --- ImportGraph/RequiredModules.lean | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 0443a42..294d745 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -126,22 +126,25 @@ partial def Environment.transitivelyRequiredModules' (env : Environment) (module for m in modules do let mut r : NameSet := {} for n in env.header.moduleData[(env.header.moduleNames.getIdx? m).getD 0]!.constNames do + -- This is messy: Mathlib is big enough that writing a recursive function causes a stack overflow. + -- So we use an explicit stack instead. We visit each constant twice: + -- once to record the constants transitively used by it, + -- and again to record the modules which defined those constants. let mut stack : Array (ConstantInfo × Option NameSet) := #[⟨← getConstInfo n, none⟩] while !stack.isEmpty do let (ci, used?) := stack.back + stack := stack.pop match used? with | none => - stack := stack.pop if !c2m.contains ci.name then let used := ci.getUsedConstantsAsSet - stack := stack.pop.push ⟨ci, some used⟩ + stack := stack.push ⟨ci, some used⟩ for u in used do if !c2m.contains u then stack := stack.push ⟨← getConstInfo u, none⟩ | some used => let transitivelyUsed : NameSet := used.fold (init := used) (fun s u => s.union ((c2m.find? u).getD {})) c2m := c2m.insert ci.name transitivelyUsed - stack := stack.pop r := r.union ((c2m.find? n).getD {}) result := result.insert m r return result