Merge branch 'nightly-testing' into bump_to_v4.17.0-rc1

ImportGraph/RequiredModules.lean

@@ -112,7 +112,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:
@@ -145,9 +145,9 @@ 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.zipWithIndex.foldl (init := {}) (fun s (n, i) => if b.getLsbD i then s.insert n else s)
+    env.header.moduleNames.zipIdx.foldl (init := {}) (fun s (n, i) => if b.getLsbD i then s.insert n else s)
 
 /--
 Return the names of the modules in which constants used in the current file were defined.