From 62b4ae0e4a9485c999291fac629cd301a4eca723 Mon Sep 17 00:00:00 2001 From: Kim Morrison Date: Thu, 30 Jan 2025 20:34:56 +1100 Subject: [PATCH] fix --- ImportGraph/RequiredModules.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/ImportGraph/RequiredModules.lean b/ImportGraph/RequiredModules.lean index 03ce248..e47707e 100644 --- a/ImportGraph/RequiredModules.lean +++ b/ImportGraph/RequiredModules.lean @@ -107,7 +107,7 @@ partial def Environment.transitivelyRequiredModules' (env : Environment) (module if verbose then IO.println s!"Processing module {m}" let mut r : BitVec N := 0 - for n in env.header.moduleData[((env.header.moduleNames.indexOf? m).map Fin.val).getD 0]!.constNames do + for n in env.header.moduleData[(env.header.moduleNames.idxOf? m).getD 0]!.constNames do if ! n.isInternal then -- 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: @@ -140,7 +140,7 @@ partial def Environment.transitivelyRequiredModules' (env : Environment) (module return result where toBitVec {N : Nat} (s : NameSet) : BitVec N := - s.fold (init := 0) (fun b n => b ||| BitVec.twoPow _ (((env.header.moduleNames.indexOf? n).map Fin.val).getD 0)) + s.fold (init := 0) (fun b n => b ||| BitVec.twoPow _ ((env.header.moduleNames.idxOf? n).getD 0)) toNameSet {N : Nat} (b : BitVec N) : NameSet := env.header.moduleNames.zipIdx.foldl (init := {}) (fun s (n, i) => if b.getLsbD i then s.insert n else s)