perf: rebuild leak on private match (#10246)

This PR prevents downstream rebuilds on changes to private `match`es
under the module system

src/Lean/Attributes.lean

@@ -165,8 +165,10 @@ def registerTagAttribute (name : Name) (descr : String)
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameSet) n => s.insert n
-    exportEntriesFn := fun es =>
+    exportEntriesFnEx := fun env es _ =>
       let r : Array Name := es.foldl (fun a e => a.push e) #[]
+      -- Do not export info for private defs
+      let r := r.filter (env.contains (skipRealize := false))
       r.qsort Name.quickLt
     statsFn         := fun s => "tag attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
     asyncMode       := asyncMode
@@ -232,8 +234,10 @@ def registerParametricAttribute (impl : ParametricAttributeImpl α) : IO (Parame
     mkInitial       := pure {}
     addImportedFn   := fun s => impl.afterImport s *> pure {}
     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2
-    exportEntriesFn := fun m =>
+    exportEntriesFnEx := fun env m _ =>
       let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[]
+      -- Do not export info for private defs
+      let r := r.filter (env.contains (skipRealize := false) ·.1)
       r.qsort (fun a b => Name.quickLt a.1 b.1)
     statsFn         := fun s => "parametric attribute" ++ Format.line ++ "number of local entries: " ++ format s.size
   }
@@ -289,8 +293,10 @@ def registerEnumAttributes (attrDescrs : List (Name × String × α))
     mkInitial       := pure {}
     addImportedFn   := fun _ _ => pure {}
     addEntryFn      := fun (s : NameMap α) (p : Name × α) => s.insert p.1 p.2
-    exportEntriesFn := fun m =>
+    exportEntriesFnEx := fun env m _ =>
       let r : Array (Name × α) := m.foldl (fun a n p => a.push (n, p)) #[]
+      -- Do not export info for private defs
+      let r := r.filter (env.contains (skipRealize := false) ·.1)
       r.qsort (fun a b => Name.quickLt a.1 b.1)
     statsFn         := fun s => "enumeration attribute extension" ++ Format.line ++ "number of local entries: " ++ format s.size
     -- We assume (and check in `modifyState`) that, if used asynchronously, enum attributes are set

src/Lean/Meta/Match/MatcherInfo.lean

@@ -87,6 +87,9 @@ builtin_initialize extension : SimplePersistentEnvExtension Entry State ←
     addEntryFn    := State.addEntry
     addImportedFn := fun es => (mkStateFromImportedEntries State.addEntry {} es).switch
     asyncMode     := .async .mainEnv
+    exportEntriesFnEx? := some fun env _ entries _ =>
+      -- Do not export info for private defs
+      entries.filter (env.contains (skipRealize := false) ·.name) |>.toArray
   }
 
 def addMatcherInfo (env : Environment) (matcherName : Name) (info : MatcherInfo) : Environment :=

tests/pkg/rebuild/test.sh

@@ -60,3 +60,11 @@ test_unchanged
 # Specializations do not matter.
 sed_i 's/x + 1/x + 2/' Rebuild/Basic.lean
 test_unchanged
+
+# private `match`es do not matter.
+cat >> Rebuild/Basic.lean <<EOF
+def matchTest : Nat -> Nat
+  | 0 => 1
+  | n+1 => n
+EOF
+test_unchanged