bootstrapping

Author: Kha

src/Lean/Compiler/InitAttr.lean

@@ -66,7 +66,11 @@ unsafe def registerInitAttrUnsafe (attrName : Name) (runAfterImport : Bool) (ref
     -- Save `meta initialize` in .olean; `initialize`s of any kind will be stored in .ir by
     -- `exportIREntries` analogously to `Lean.IR.declMapExt` so we can run them when meta-imported,
     -- even without the .olean file.
-    filterExport := fun env declName _ => runAfterImport && isMeta env declName
+    filterExport := fun env declName _ =>
+      -- TODO: The interpreter currently depends on `[builtin_init]` to be exported for
+      -- `prefer_native` handling but this is incorrect with private imports anyway and should be
+      -- replaced by consulting a builtin list.
+      !runAfterImport || isMeta env declName
   }
 
 @[implemented_by registerInitAttrUnsafe]