chore: ignore autoparam declarations in private module linter

[thorimur]

Autogenerated declarations for the syntax of autoparams never start with _private, and thus are in some sense always public. We manually exclude them from the class of public declarations here.

Note that something like isInternalDetail is too strong; that would also exclude public declarations generated by initialize, which ought to be considered bona-fide public declarations.

We add @[expose] public section to Mathlib.Analysis.Normed.Lp.SmoothApprox.

---

[github-actions]

PR summary 151fb3b204

Import changes for modified files

No significant changes to the import graph

Import changes for all files

Files	Import difference

---

Declarations diff

No declarations were harmed in the making of this PR! 🐙

You can run this locally as follows

## summary with just the declaration names:
./scripts/declarations_diff.sh <optional_commit>

## more verbose report:
./scripts/declarations_diff.sh long <optional_commit>

The doc-module for script/declarations_diff.sh contains some details about this script.

---

No changes to technical debt.

You can run this locally as

./scripts/technical-debt-metrics.sh pr_summary

• The relative value is the weighted sum of the differences with weight given by the inverse of the current value of the statistic.
• The absolute value is the relative value divided by the total sum of the inverses of the current values (i.e. the weighted average of the differences).

[grunweg]

Thank you for the prompt investigation and making at least a band-aid fix! If this works, you should see CI fail because of Mathlib.Analysis.Normed.Lp.SmoothApprox --- and I'll be curious what else it finds. Let's wait for the zulip thread to conclude before merging.

[thorimur]

I've now tested not counting any isInternalDetail name as public, and I believe that this is not the right move. :) I listed the constants from everything except Mathlib.Analysis.Normed.Lp.SmoothApprox, and found:

[(initFn✝, Mathlib.Combinatorics.Matroid.Init),
 (initFn✝, Mathlib.Combinatorics.SimpleGraph.Init),
 (initFn✝, Mathlib.Data.Finset.Attr),
 (initFn✝, Mathlib.Tactic.ArithMult.Init),
 (and_imp._simp_2, Mathlib.Tactic.Attr.Core),
 (not_false._simp_1, Mathlib.Tactic.Attr.Core),
 (eq_iff_true_of_subsingleton._simp_1, Mathlib.Tactic.Attr.Core),
 (forall_const._simp_2, Mathlib.Tactic.Attr.Core),
 (initFn✝, Mathlib.Tactic.Bound.Init),
 (initFn✝, Mathlib.Tactic.Continuity.Init),
 (initFn✝, Mathlib.Tactic.Finiteness.Attr),
 (initFn✝, Mathlib.Tactic.Measurability.Init),
 (initFn✝, Mathlib.Topology.Sheaves.Init),
 (initFn✝, Mathlib.Data.Sym.Sym2.Init)]

We should indeed always consider initFns from initialize as genuine public declarations, and the ones in Mathlib.Tactic.Attr.Core are generated by @[mfld_simps] and @[nontriviality] in a public section (which I believe also counts).

Code:

module

import Mathlib.Tactic.Attr.Core
import Mathlib.Tactic.Bound.Init
import Mathlib.Tactic.Measurability.Init
import Mathlib.Tactic.ArithMult.Init
import Mathlib.Combinatorics.Matroid.Init
import Mathlib.Combinatorics.SimpleGraph.Init
import Mathlib.Data.Sym.Sym2.Init
import Mathlib.Topology.Sheaves.Init
import Mathlib.Data.Finset.Attr
import Mathlib.Tactic.Continuity.Init
import Mathlib.Tactic.Finiteness.Attr

open Lean

def modNames := #[
  `Mathlib.Tactic.Attr.Core,
  `Mathlib.Tactic.Bound.Init,
  `Mathlib.Tactic.Measurability.Init,
  `Mathlib.Tactic.ArithMult.Init,
  `Mathlib.Combinatorics.Matroid.Init,
  `Mathlib.Combinatorics.SimpleGraph.Init,
  `Mathlib.Data.Sym.Sym2.Init,
  `Mathlib.Topology.Sheaves.Init,
  `Mathlib.Data.Finset.Attr,
  `Mathlib.Tactic.Continuity.Init,
  `Mathlib.Tactic.Finiteness.Attr
]

run_cmd do
  let env ← getEnv
  let modIdxs? := modNames.map fun n =>
    env.header.moduleNames.findIdx? (· == n)
  if modIdxs?.any (·.isNone) then throwError "could not find some module"
  let mut importedConsts := #[]
  for (name,_) in (← getEnv).constants.map₁ do
    if let some idx := modIdxs?.idxOf? <| (← getEnv).getModuleIdxFor? name then
      importedConsts := importedConsts.push (MessageData.ofConstName name, modNames[idx]!)
  logInfo m!"{importedConsts.qsort (·.2.lt ·.2)}"

[grunweg]

Do you think it's easy to add a test for initialize declarations? If so, do you mind doing so as well? Let's keep this tested while we still remember the details.

[thorimur]

Ah, good point. :)

[thorimur]

I've rescinded the comment about simp, because I've realized these attributes are not as generative as simps despite containing simps in the name, but are instead just simp sets. 🙃 It is perhaps another question as to whether we want to consider public changes to a simp set as meaningfully "public". (I wonder if there's a way to detect whether we've made "public changes to the environment"? 🤔) And perhaps that's outside of the scope of this fix.

[thorimur]

This issue will be fixed in lean4#11581, so let's close this. I'll move the initialize test and @[expose] public section to other PRs. :) EDIT: apparently @[expose] public section was added in #32566 :)

initialize test in #32695

[thorimur]

Actually, just to consider all possibilities: @grunweg, do you think we ought to have this as a temporary fix before lean4#11581 lands in mathlib (and change the documentation to describe it as such), then clean it up later? Do you know approximately how long it will be before the fix makes its way to mathlib, assuming it's merged shortly? I'd rather spare the churn, but if it'll be a while... :)

[grunweg]

The fix got merged already, so that part is clear :-) If it's backported, it can be in next week's release (i.e., land in mathlib in roughly a week); otherwise a week longer. I've asked on zulip.