PrivateModule linter not firing

Stream: mathlib4

[Michael Rothgang]

We have a new privateModule linter in mathlib (which is great!). However, it doesn't fire on #30998 --- which seemingly adds no public declarations at all. I did check: this branch includes the linter, and the mathlib standard linter set is enabled at that point.

Can anybody help me investigate?

[Michael Rothgang]

I've made #32128 to start debugging that file (currently waiting for CI to build olean's).

[Junyan Xu]

It's not firing on #32080 either

[Junyan Xu]

... (consequently?) the docBlame linter also isn't triggering on this def.

[Damiano Testa]

I think that the new module system has changed so much of the infrastructure that probably we should revise all linters to check that they still work as expected.

[Michael Rothgang]

Sure, but that linter was written after mathlib moved to the module system :sweat_smile:

[Damiano Testa]

I know, but I still think that I have not understood how things work, so I probably did not pick up potential issues...

[Michael Rothgang]

CI results are in, and with a bit of debugging I found something interesting:

• (← getEnv).constants.map₂ in the linter actually reports a public declaration, namely docs#MvPolynomial.eq_1
• however, #check MvPolynomial.eq_1already is defined at the start of the module

[Michael Rothgang]

Does that indicate a bug in Environment.constants.map₂?

[Johan Commelin]

cc @Sebastian Ullrich ?

[Michael Rothgang]

And MvPolynomial.eq_1 is not hoverable, so I'm not sure where it's defined.

[Johan Commelin]

Probably at docs#MvPolynomial

[Michael Rothgang]

Indeed: #check MvPolynomial.eq_1 works right after the definition, but not before.

[Aaron Liu]

Michael Rothgang said:

CI results are in, and with a bit of debugging I found something interesting:

• (← getEnv).constants.map₂ in the linter actually reports a public declaration, namely docs#MvPolynomial.eq_1
• however, #check MvPolynomial.eq_1already is defined at the start of the module

What do you get from whatsnew in #print MvPolynomial.eq_1? This is one of those lemmas that doesn't exist until you use it.

[Michael Rothgang]

Putting this right after docs#MvPolynomial yields the following

/--
info: @[defeq] theorem MvPolynomial.eq_1.{u_1, u_2} : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R],
  MvPolynomial σ R = R[σ →₀ ℕ] :=
fun σ R [CommSemiring R] ↦ Eq.refl (MvPolynomial σ R)
---
info: theorem MvPolynomial.eq_1.{u_1, u_2} : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R],
  MvPolynomial σ R = R[σ →₀ ℕ] :=
fun σ R [CommSemiring R] ↦ Eq.refl (MvPolynomial σ R)

-- Lean.declRangeExt extension: 0 new entries

-- Lean.docStringExt extension: 0 new entries

-- _private.Lean.DocString.Extension.0.Lean.inheritDocStringExt extension: 0 new entries

-- Lean.versoDocStringExt extension: 0 new entries

-- _private.Lean.Compiler.MetaAttr.0.Lean.declMetaExt extension: 0 new entries

-- Lean.Compiler.inlineAttrs extension: 0 new entries

-- Lean.projectionFnInfoExt extension: 0 new entries

-- _private.Lean.AddDecl.0.Lean.privateConstKindsExt extension: 1 new entries

-- Lean.Compiler.LCNF.baseExt extension: 0 new entries

-- Lean.Compiler.LCNF.monoExt extension: 0 new entries

-- Lean.IR.declMapExt extension: 0 new entries

-- Lean.IR.UnreachableBranches.functionSummariesExt extension: 0 new entries

-- Lean.Compiler.LCNF.Simp.ConstantFold.folderExt extension: 0 new entries

-- Lean.Compiler.LCNF.specExtension extension: 0 new entries

-- Lean.Compiler.LCNF.Specialize.specCacheExt extension: 0 new entries

-- Lean.Compiler.LCNF.UnreachableBranches.functionSummariesExt extension: 0 new entries

-- Lean.extraModUses extension: 0 new entries

-- Lean.defeqAttr extension: 1 new entries

-- Lean.Meta.congrKindsExt extension: 0 new entries

-- Lean.Elab.Structural.eqnInfoExt extension: 0 new entries

-- Lean.Server.userRpcProcedures extension: 0 new entries

-- Lean.Elab.WF.eqnInfoExt extension: 0 new entries

-- Lean.Elab.PartialFixpoint.eqnInfoExt extension: 0 new entries

-- Lean.Meta.funIndInfoExt extension: 0 new entries
-/
#guard_msgs in
whatsnew in #print MvPolynomial.eq_1

[Aaron Liu]

Yeah see it's new

[Aaron Liu]

What if you put it at the end of the file?

[Michael Rothgang]

Perhaps the private module linter is doing the wrong check: it does !isPrivateName decl...

[Michael Rothgang]

Aaron Liu said:

What if you put it at the end of the file?

At the end of MvPolynomial.Basic: same out

[Michael Rothgang]

At the beginning of FieldTheory/SeparatablyGenerated (the module where the linter does not fire): slightly different, but very similar output

/--
info: @[defeq] theorem MvPolynomial.eq_1.{u_1, u_2} : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R],
  MvPolynomial σ R = AddMonoidAlgebra R (σ →₀ ℕ) :=
fun σ R [CommSemiring R] ↦ Eq.refl (MvPolynomial σ R)
---
info: theorem MvPolynomial.eq_1.{u_1, u_2} : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R],
  MvPolynomial σ R = AddMonoidAlgebra R (σ →₀ ℕ) :=
fun σ R [CommSemiring R] ↦ Eq.refl (MvPolynomial σ R)

-- Lean.declRangeExt extension: 0 new entries

-- Lean.docStringExt extension: 0 new entries

-- _private.Lean.DocString.Extension.0.Lean.inheritDocStringExt extension: 0 new entries

-- Lean.versoDocStringExt extension: 0 new entries

-- _private.Lean.Compiler.MetaAttr.0.Lean.declMetaExt extension: 0 new entries

-- Lean.Compiler.inlineAttrs extension: 0 new entries

-- Lean.projectionFnInfoExt extension: 0 new entries

-- _private.Lean.AddDecl.0.Lean.privateConstKindsExt extension: 1 new entries

-- Lean.Compiler.LCNF.baseExt extension: 0 new entries

-- Lean.Compiler.LCNF.monoExt extension: 0 new entries

-- Lean.IR.declMapExt extension: 0 new entries

-- Lean.IR.UnreachableBranches.functionSummariesExt extension: 0 new entries

-- Lean.Compiler.LCNF.Simp.ConstantFold.folderExt extension: 0 new entries

-- Lean.Compiler.LCNF.specExtension extension: 0 new entries

-- Lean.Compiler.LCNF.Specialize.specCacheExt extension: 0 new entries

-- Lean.Compiler.LCNF.UnreachableBranches.functionSummariesExt extension: 0 new entries

-- Lean.extraModUses extension: 0 new entries

-- Lean.defeqAttr extension: 1 new entries

-- Lean.Meta.congrKindsExt extension: 0 new entries

-- Lean.Elab.Structural.eqnInfoExt extension: 0 new entries

-- Lean.Server.userRpcProcedures extension: 0 new entries

-- Lean.Elab.WF.eqnInfoExt extension: 0 new entries

-- Lean.Elab.PartialFixpoint.eqnInfoExt extension: 0 new entries

-- Lean.Meta.funIndInfoExt extension: 0 new entries
-/
#guard_msgs in
whatsnew in #print MvPolynomial.eq_1

[Aaron Liu]

sorry, I mean put it at the end of the file where the linter didn't lint

[Michael Rothgang]

I was wondering if you meant that :-)

/--
info: @[defeq] theorem MvPolynomial.eq_1.{u_1, u_2} : ∀ (σ : Type u_1) (R : Type u_2) [inst : CommSemiring R],
  MvPolynomial σ R = AddMonoidAlgebra R (σ →₀ ℕ) :=
fun σ R [CommSemiring R] ↦ Eq.refl (MvPolynomial σ R)
---
info: -- Lean.declRangeExt extension: 0 new entries
-- Lean.docStringExt extension: 0 new entries
-- _private.Lean.DocString.Extension.0.Lean.inheritDocStringExt extension: 0 new entries
-- Lean.versoDocStringExt extension: 0 new entries
-- _private.Lean.Compiler.MetaAttr.0.Lean.declMetaExt extension: 0 new entries
-- Lean.Compiler.inlineAttrs extension: 0 new entries
-- Lean.projectionFnInfoExt extension: 0 new entries
-- _private.Lean.AddDecl.0.Lean.privateConstKindsExt extension: 0 new entries
-- Lean.Compiler.LCNF.baseExt extension: 0 new entries
-- Lean.Compiler.LCNF.monoExt extension: 0 new entries
-- Lean.IR.declMapExt extension: 0 new entries
-- Lean.IR.UnreachableBranches.functionSummariesExt extension: 0 new entries
-- Lean.Compiler.LCNF.Simp.ConstantFold.folderExt extension: 0 new entries
-- Lean.Compiler.LCNF.specExtension extension: 0 new entries
-- Lean.Compiler.LCNF.Specialize.specCacheExt extension: 0 new entries
-- Lean.Compiler.LCNF.UnreachableBranches.functionSummariesExt extension: 0 new entries
-- Lean.extraModUses extension: 0 new entries
-- Lean.defeqAttr extension: 0 new entries
-- Lean.Meta.congrKindsExt extension: 0 new entries
-- Lean.Elab.Structural.eqnInfoExt extension: 0 new entries
-- Lean.Server.userRpcProcedures extension: 0 new entries
-- Lean.Elab.WF.eqnInfoExt extension: 0 new entries
-- Lean.Elab.PartialFixpoint.eqnInfoExt extension: 0 new entries
-- Lean.Meta.funIndInfoExt extension: 0 new entries
-/
#guard_msgs in
whatsnew in #print MvPolynomial.eq_1

[Michael Rothgang]

In particular, all lines say "0 new entries"

[Sebastian Ullrich]

Ah, the linter should filter out any isReservedNames

[Aaron Liu]

So at the end of the file it's not new anymore

[Aaron Liu]

see it's not printing the theorem declaration twice

[Aaron Liu]

so this is definitely defined somewhere in the file

[Michael Rothgang]

So the linter should read if !isPrivateName decl && !isReservedName (← getEnv) decl then instead of the current if !isPrivateName decl then?

[Sebastian Ullrich]

Yes, that's more correct and possibly also fully correct :)

[Sebastian Ullrich]

It is hard to make a statement about the behavior of any and all involved metaprograms, especially when some might not be from core

[Michael Rothgang]

#32140 fixes the linter. It would be very nice to add a test; can somebody help me by suggesting one (that's not "take this entire module in mathlib")?

[Aaron Liu]

Junyan Xu said:

It's not firing on #32080 either

That's because I have public theorems

[Aaron Liu]

Junyan Xu said:

... (consequently?) the docBlame linter also isn't triggering on this def.

That's because it's private

[Junyan Xu]

I see, decls are by default private now. @[expose] public section restores the old behavior.

[Thomas Murrills]

(Great to wake up to both a bug and its fix! :grinning_face_with_smiling_eyes:)

Hmm, what about some of the things isAutoDecl checks? Obviously some are simply evidence of public declarations, and there is no need to consider them private—but specifically, I could imagine considering as "private"

• isInternal names
• names which have macro scopes
• names which start with match_ or proof_

I'm not sure if these are already covered by existing checks, though: for instance, it seems like a match_* lemma is _private iff it's generated by a private declaration, but I'm not sure. (Note: it's not reserved)

[Michael Rothgang]

Good points, for all of these. Do you have examples at hand? It would be great to verify these, and having an example to look at would also make it much easier for me to decide what sensible behaviour would be.

[Sebastian Ullrich]

If a public declaration is synthesized from a private one, that should likely be considered a bug in that metaprogram. This is true for reserved names as well but the special thing about them is that the two decls can live in different files, so it makes sense for the linter to special case them.

[Michael Rothgang]

I just found a new case of this: file#Mathlib.Analysis.Normed.Lp.SmoothApprox seems to define no public file, but is fine. Does somebody here have time to investigate? (I probably won't, in the near future, sadly.)

[Michael Rothgang]

Correct link: https://github.com/leanprover-community/mathlib4/blob/master/Mathlib/Analysis/Normed/Lp/SmoothApprox.lean

[Michael Rothgang]

#32128 should have debugging output in around an hour, which should make investigating not so difficult

[Moritz Doll]

It seems that the linter finds some weird declarations, even if nothing is public:

privateModule linter is running
found public declaration _auto._@.Mathlib.Analysis.Normed.Lp.SmoothApprox.2780282558._hygCtx._hyg.36
found public declaration _auto._@.Mathlib.Analysis.Normed.Lp.SmoothApprox.2871035219._hygCtx._hyg.37

[Moritz Doll]

With @[expose] public section we get all of the actual declarations on top

privateModule linter is running
found public declaration _auto._@.Mathlib.Analysis.Normed.Lp.SmoothApprox.2780282558._hygCtx._hyg.36
found public declaration _auto._@.Mathlib.Analysis.Normed.Lp.SmoothApprox.2871035219._hygCtx._hyg.37
found public declaration HasCompactSupport.exist_eLpNorm_sub_le_of_continuous
found public declaration MeasureTheory.MemLp.exist_eLpNorm_sub_le
found public declaration MeasureTheory.Lp.dense_hasCompactSupport_contDiff

[Moritz Doll]

it seems that by volume_tac is the problem

[Michael Rothgang]

That's interesting; it seems we found a new bug in the linter :tada:

[Michael Rothgang]

What happens when you do #whatsnew on the new declarations? (Similarly to the debugging further up this thread.)

[Moritz Doll]

If I check with Batteries.Tactic.Lint.isAutoDecl as well, then it is fine

[Michael Rothgang]

@Thomas Murrills It seems there's another bug - in this linter or in volume_tac.

[Moritz Doll]

          if !isPrivateName decl && !isReservedName (← getEnv) decl && !(← liftCoreM (Batteries.Tactic.Lint.isAutoDecl decl)) then

[Moritz Doll]

In the doc-string it says that this check is not done on purpose, so either volume_tac does something wrong or the linter has to be more strict

[Michael Rothgang]

Exactly - but I don't know enough Lean internals to say for sure which one.

[Moritz Doll]

volume_tac is just

/-- The tactic `exact volume`, to be used in optional (`autoParam`) arguments. -/
macro "volume_tac" : tactic =>
  `(tactic| (first | exact MeasureTheory.MeasureSpace.volume))

so I feel out of my depth as well

[Michael Rothgang]

For my own curiousity: does the linter still not fire if you replace the tactic by exact MeasureTheory.MeasureSpace.volume?

[Moritz Doll]

yeah, that does not make a difference

[Moritz Doll]

i.e., replace by volume_tac by by exact volume yields the same results (I was in fact wondering why there is the first | .. in the tactic)

[Moritz Doll]

seems a bit redundant (#32586)

[Thomas Murrills]

Hmm, nice investigation! :) These _auto declarations are public in the given module, but are they indeed ultimately imported downstream as you’d expect? (Or do lean internals e.g. ignore things with macro scopes when exporting?)

[Thomas Murrills]

(I can investigate this in about an hour if no one gets to it.)

[Thomas Murrills]

Basically, if they are imported downstream, that seems to me like a meta bug arising from volume_tac somehow. If they’re not, it means we need another check—perhaps macro scopes, or perhaps isInternal. (In this case we should see what core does.)

(It could also be the case that these are deliberately allowed to leak into the public scope because they’re inaccessible to the user anyway, given that they have macro scopes or are internal, but I’d be surprised. But I’ve been surprised before! :) )

[Thomas Murrills]

Interestingly, the following:

module

import Mathlib.Analysis.Normed.Lp.SmoothApprox

open Lean

run_cmd do
  let modIdx? := (← getEnv).header.moduleNames.findIdx?
      (· == `Mathlib.Analysis.Normed.Lp.SmoothApprox)
  if modIdx?.isNone then throwError "could not find module"
  let mut fromSmoothApprox := #[]
  for (name,_) in (← getEnv).constants.map₁ do
    if (← getEnv).getModuleIdxFor? name == modIdx? then
      fromSmoothApprox := fromSmoothApprox.push name
  logInfo m!"{fromSmoothApprox.map MessageData.ofConstName}"

yields

[_private.Mathlib.Analysis.Normed.Lp.SmoothApprox.0.MeasureTheory.MemLp.exist_eLpNorm_sub_le,
 _auto._@.Mathlib.Analysis.Normed.Lp.SmoothApprox.2780282558._hygCtx._hyg.36,
 _private.Mathlib.Analysis.Normed.Lp.SmoothApprox.0.MeasureTheory.Lp.dense_hasCompactSupport_contDiff,
 _auto._@.Mathlib.Analysis.Normed.Lp.SmoothApprox.2871035219._hygCtx._hyg.37,
 _private.Mathlib.Analysis.Normed.Lp.SmoothApprox.0.HasCompactSupport.exist_eLpNorm_sub_le_of_continuous]

So, it seems like the private constants are "imported" as well, but they have that num component (0) in the middle. I'm therefore not sure that having these in the imported constants means anything...maybe there's a more appropriate way to check if a constant is "imported".

[Thomas Murrills]

Note: it seems that this is not a property of volume_tac, but of any autoParam. (Indeed, by skip produces similar decls.) I was under the impression before looking at the code that volume_tac was being executed. However, these _auto declarations are in fact autogenerated declarations reperesenting the Syntax of the autoparam! (Hover over them after running the code above to see their type.)

[Thomas Murrills]

(Note: the meta declaration which constructs these declarations is Lean.Elab.Term.declareTacticSyntax.)

[Thomas Murrills]

For what it's worth, it seems that this declaration is generated at variable, and then again at every theorem that uses it (which is only one).

[Thomas Murrills]

I would like to check to see if autoparams are in fact intended to be exported like this in lean core, but in the meantime, the most limited possible fix is simply not counting names with the prefix _auto (which is added by declareTacticSyntax.

Alternatively, we could avoid counting all names that are inaccessible to the user: isInternalOrNum should do it. (Note: this subsumes hasMacroScopes.)

However, the part of the docstring of isInternalOrNum which states that "the frontend does not allow user declarations to start with _ in any of its parts" does not seem to be true...

[Thomas Murrills]

:working_on_it: #32597; starting with the limited-scope fix, will test the broader strategy as well.

[Thomas Murrills]

I've asked about these decls in #lean4 > Should autoparam helper decls be private? .

[Thomas Murrills]

I've now tested not counting names which satisfy isInternalDetail as public, and I am pretty sure this is not what we want, as it means not counting initialize declarations and lemmas generated by simps-esque attributes as public. (More info in PR comments.)

It's also possible that we do not get resolution on this question until Sebastian comes back from traveling, so I suggest we go ahead with just excluding _auto for now. :) I've also mentioned the lean issue (lean4#11569) in the PR.

[Michael Rothgang]

Another instance: #31732 was also missed by the linter. It doesn't look like it has any autoparams --- is this another bug? @Thomas Murrills

[Michael Rothgang]

(Be my guest to modify my debugging PR!)

[Thomas Murrills]

Aux decls generated by notation3 seem to be the culprit. :) I think this falls under the scope of "bug in the metaprogram" (i.e., notation3 is not respecting visibility). Seeing if I can fix it easily now. :)

[Thomas Murrills]

For some reason it explicitly makes the delab public...?

public aux_def delab_app $(mkIdent fullName) : Delab :=

[Thomas Murrills]

Ah, it seems this was just during the bump, which is understandable. :)

[Thomas Murrills]

#32749 fixes notation3 and adds a test for the private module linter. (Assuming it passes CI. :grinning_face_with_smiling_eyes:)

[Michael Rothgang]

CI fails in the tests, but for a reason that's not obvious to me.

[Ruben Van de Velde]

Restarted the job, who knows

[Thomas Murrills]

Oops, sorry, that was actually just me not committing everything I intended to! :upside_down:

[Thomas Murrills]

CI is green now. :)