feat: do not report metaprogramming declarations via exact? and rw?

[kim-em]

This PR filters out all declarations from Lean.*, *.Tactic.*, and *.Linter.* from the results of exact? and rw?.

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase f01527142e1df55c060b9abb6a36b3606ffa6ada --onto f4c9934171a22d376fb7c318ce2dcf80ab0eaf0e. (2025-01-16 23:00:38)

[nomeata]

This conflicts a bit of using Lean.Order for a theory that is not general purpose (hence the name Lean) and really only for one feature partial_fixpoint, but it is meant to be extensible by users who may have to prove theorems.

As a pragmatic compromise, could isMetaprogramming live in CoreM and do not filter out names from explicitly opened namespaces? If I am in open Lean.Order, then I’m probably interested in these lemmas.

Or I change my naming convention in #6355 to something else.

[nomeata]

Another way to shave the cat:

We introduce an way to mark namespaces (not names) as “hidden”. This annotation should convey that contents of the namespace should not show up in search results, autocompletion etc., unless that namespaces is explicitly opened. This would also work well for Lean.Grind, can be used by libraries, and it a bit more precise than my previous suggestion (where a blunt open Lean might already unhide too much).

[kim-em]

I suspect for exact? at least we'd have to plumb things differently to respect open namespaces, as we couldn't be looking that up for each declaration. But it would be doable.

If it's possible to just use the Lean.* boundary, I'd prefer that...

[nomeata]

I suspect for exact? at least we'd have to plumb things differently to respect open namespaces, as we couldn't be looking that up for each declaration. But it would be doable.

Is this filtering just for presentation or also for the search? I.e. could you filter the successful results and maybe even include a hint (“some results from hidden namespaces were omitted“). That may be both good (users find a proof, and can copy some theorem or ask for a public one) and bad (users enable +hidden and use the internal proof again).

If it's possible to just use the Lean.* boundary, I'd prefer that...

Ok. If we are doing ad-hoc things I can ex-exclude Lean.Order when I land that :-)

[adomani]

Suggested change

	/-- Return true if the name is in a namespace associated to metaprogramming.-/
	/-- Return true if the name is in a namespace associated to metaprogramming. -/

[adomani]

The environment linters in Batteries use Batteries.Tactic.Lint as part of their namespace: they get excluded by Tactic, but maybe you could

• also filter Lint here, or
• change their namespace to Linter instead of Lint.

[adomani]

Suggested change

	-- If this lemmas is added later to the library, please update this `#guard_msgs`.
	-- If this lemma is added later to the library, please update this `#guard_msgs`.