diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 535ea787e0..fb27863e8f 100644 --- a/src/Lean/Attributes.lean +++ b/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 := { diff --git a/src/Lean/Compiler/IR/CompilerM.lean b/src/Lean/Compiler/IR/CompilerM.lean index e601bce70c..75440509ce 100644 --- a/src/Lean/Compiler/IR/CompilerM.lean +++ b/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 diff --git a/src/Lean/Compiler/InitAttr.lean b/src/Lean/Compiler/InitAttr.lean index 7713065e71..c2998f9db0 100644 --- a/src/Lean/Compiler/InitAttr.lean +++ b/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. diff --git a/tests/pkg/initialize/Initialize.lean b/tests/pkg/initialize/Initialize.lean index e205e2493a..a2cf53b50e 100644 --- a/tests/pkg/initialize/Initialize.lean +++ b/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 diff --git a/tests/pkg/initialize/Initialize/Basic.lean b/tests/pkg/initialize/Initialize/Basic.lean index d25d1eed68..4b7e4ae576 100644 --- a/tests/pkg/initialize/Initialize/Basic.lean +++ b/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") diff --git a/tests/pkg/initialize/Initialize/Module.lean b/tests/pkg/initialize/Initialize/Module.lean new file mode 100644 index 0000000000..60a698329e --- /dev/null +++ b/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 diff --git a/tests/pkg/initialize/Initialize/NoModule.lean b/tests/pkg/initialize/Initialize/NoModule.lean new file mode 100644 index 0000000000..538df82ddb --- /dev/null +++ b/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