experiment: try recording all name resolutions

src/Lean/Elab/Open.lean

@@ -17,7 +17,7 @@ namespace OpenDecl
 
 variable [Monad m] [STWorld IO.RealWorld m] [MonadEnv m]
 variable [MonadExceptOf Exception m] [MonadRef m] [AddErrorMessageContext m]
-variable [AddMessageContext m] [MonadLiftT (ST IO.RealWorld) m] [MonadLog m]
+variable [AddMessageContext m] [MonadLiftT (ST IO.RealWorld) m] [MonadLog m] [MonadTrace m]
 
 /--
 A local copy of name resolution state that allows us to immediately use new open decls

src/Lean/ExtraModUses.lean

@@ -6,7 +6,7 @@ Authors: Sebastian Ullrich
 module
 
 prelude
-public import Lean.CoreM
+public import Lean.Util.Trace
 public import Lean.Compiler.MetaAttr  -- TODO: public because of specializations
 
 /-!

src/Lean/ResolveName.lean

@@ -10,6 +10,7 @@ public import Lean.Modifiers
 public import Lean.Exception
 public import Lean.Namespace
 public import Lean.Log
+public import Lean.ExtraModUses
 
 public section
 
@@ -267,7 +268,7 @@ instance (m n) [MonadLift m n] [MonadResolveName m] : MonadResolveName n where
   getOpenDecls     := liftM (m:=m) getOpenDecls
 
 variable [Monad m] [MonadResolveName m] [MonadEnv m] [MonadOptions m] [MonadLog m] [AddMessageContext m]
-  [MonadError m]
+  [MonadError m] [MonadTrace m]
 
 def checkPrivateInPublic (id : Name) : m Unit := do
   if (← getEnv).isExporting && isPrivateName id && (← ResolveName.backward.privateInPublic.warn.getM) then
@@ -320,6 +321,8 @@ called incidentally or multiple times.
 -/
 def resolveGlobalName (id : Name) (enableLog := true) : m (List (Name × List String)) := do
   let res := ResolveName.resolveGlobalName (← getEnv) (← getOptions) (← getCurrNamespace) (← getOpenDecls) id
+  for (n, _) in res do
+    recordExtraModUseFromDecl (isMeta := false) n
   -- `isExporting` is already checked in `checkPrivateInPublic` but should be cheaper than `isPrivateName`
   if enableLog && (← getEnv).isExporting then
     if let some prv := res.find? (isPrivateName ·.1) then