diff --git a/src/Lean/Attributes.lean b/src/Lean/Attributes.lean index 2ba0b3f982..5f85872fa0 100644 --- a/src/Lean/Attributes.lean +++ b/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 diff --git a/src/Lean/Meta/Match/MatcherInfo.lean b/src/Lean/Meta/Match/MatcherInfo.lean index a886a136b2..2f05131d15 100644 --- a/src/Lean/Meta/Match/MatcherInfo.lean +++ b/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 := diff --git a/tests/pkg/rebuild/test.sh b/tests/pkg/rebuild/test.sh index e492e024df..a32f6747ee 100755 --- a/tests/pkg/rebuild/test.sh +++ b/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 < Nat + | 0 => 1 + | n+1 => n +EOF +test_unchanged