fix: use resolveGlobalConstNoOverload at init attribute handler

src/Lean/Compiler/InitAttr.lean

@@ -26,6 +26,7 @@ registerParametricAttribute `init "initialization procedure for global reference
   decl ← getConstInfo declName;
   match attrParamSyntaxToIdentifier stx with
   | some initFnName => do
+    initFnName ← resolveGlobalConstNoOverload initFnName;
     initDecl ← getConstInfo initFnName;
     match getIOTypeArg initDecl.type with
     | none => throwError ("initialization function '" ++ initFnName ++ "' must have type of the form `IO <type>`")

tests/compiler/init.lean

@@ -1,5 +1,7 @@
 new_frontend
 
+namespace Foo
+
 initialize ref : IO.Ref Nat ← IO.mkRef 10
 
 initialize vals : IO.Ref (Array String) ← IO.mkRef #[]
@@ -20,6 +22,9 @@ initialize
 initialize
   registerVal "foo"
 
+end Foo
+open Foo
+
 def main : IO Unit := do
 IO.println "hello world"
 IO.println (← ref.get)