fix: run @[init] declarations in declaration order (#12221)

Fixes #10175 harder.

src/Lean/Attributes.lean

@@ -270,10 +270,11 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
       let mut r := if impl.preserveOrder then
         decls.toArray.reverse.filterMap (fun n => return (n, ← m.find? n))
       else
-        m.foldl (fun a n p => a.push (n, p)) #[]
+        let r := m.foldl (fun a n p => a.push (n, p)) #[]
+        r.qsort (fun a b => Name.quickLt a.1 b.1)
       if lvl != .private then
         r := r.filter (fun ⟨n, a⟩ => impl.filterExport env n a)
-      r.qsort (fun a b => Name.quickLt a.1 b.1)
+      r
     statsFn         := fun (_, m) => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format m.size
   }
   let attrImpl : AttributeImpl := {

src/Lean/Compiler/IR/CompilerM.lean

@@ -115,10 +115,10 @@ private def exportIREntries (env : Environment) : Array (Name × Array EnvExtens
   -- safety: cast to erased type
   let irEntries : Array EnvExtensionEntry := unsafe unsafeCast <| sortDecls irDecls
 
-  -- see `regularInitAttr.filterExport`
-  let initDecls : Array (Name × Name) := regularInitAttr.ext.getState env
-      |>.2.foldl (fun a n p => a.push (n, p)) #[]
-      |>.qsort (fun a b => Name.quickLt a.1 b.1)
+  -- save all initializers independent of meta/private. Non-meta initializers will only be used when
+  -- .ir is actually loaded, and private ones iff visible.
+  let initDecls : Array (Name × Name) :=
+    regularInitAttr.ext.exportEntriesFn env (regularInitAttr.ext.getState env) .private
   -- safety: cast to erased type
   let initDecls : Array EnvExtensionEntry := unsafe unsafeCast initDecls
 

src/Lean/Compiler/InitAttr.lean

@@ -174,8 +174,11 @@ private unsafe def runInitAttrs (env : Environment) (opts : Options) : IO Unit :
         continue
       interpretedModInits.modify (·.insert mod)
       let modEntries := regularInitAttr.ext.getModuleEntries env modIdx
-      -- `getModuleIREntries` is identical to `getModuleEntries` if we loaded only one of .olean/.ir
-      -- so deduplicate (these lists should be very short)
+      -- `getModuleIREntries` is identical to `getModuleEntries` if we loaded only one of
+      -- .olean (from `meta initialize`)/.ir (`initialize` via transitive `meta import`)
+      -- so deduplicate (these lists should be very short).
+      -- If we have both, we should not need to worry about their relative ordering as `meta` and
+      -- non-`meta` initialize should not have interdependencies.
       let modEntries := modEntries ++ (regularInitAttr.ext.getModuleIREntries env modIdx).filter (!modEntries.contains ·)
       for (decl, initDecl) in modEntries do
         -- Skip initializers we do not have IR for; they should not be reachable by interpretation.

tests/pkg/initialize/Initialize.lean

@@ -1,5 +1,2 @@
-import Initialize.Basic
-
-/-- info: 42 -/
-#guard_msgs in
-#eval initNat
+import Initialize.Module
+import Initialize.NoModule

tests/pkg/initialize/Initialize/Basic.lean

@@ -1 +1,10 @@
-initialize initNat : Nat ← pure 42
+module
+
+public initialize initNat : Nat ← pure 42
+
+public initialize ref : IO.Ref (Array String) ← IO.mkRef #[]
+
+initialize ref3 : Unit ← ref.modify (·.push "ref3")
+public initialize ref2 : Unit ← ref.modify (·.push "ref2")
+public initialize ref1 : Unit ← ref.modify (·.push "ref1")
+initialize ref4 : Unit ← ref.modify (·.push "ref4")

tests/pkg/initialize/Initialize/Module.lean

@@ -0,0 +1,11 @@
+module
+
+meta import Initialize.Basic
+
+/-- info: 42 -/
+#guard_msgs in
+#eval initNat
+
+/-- info: #["ref3", "ref2", "ref1", "ref4"] -/
+#guard_msgs in
+#eval ref.get

tests/pkg/initialize/Initialize/NoModule.lean

@@ -0,0 +1,9 @@
+import Initialize.Basic
+
+/-- info: 42 -/
+#guard_msgs in
+#eval initNat
+
+/-- info: #["ref3", "ref2", "ref1", "ref4"] -/
+#guard_msgs in
+#eval ref.get