Should autoparam helper decls be private?

Stream: lean4

[Thomas Murrills]

It was noticed in #mathlib4 > PrivateModule linter not firing @ 💬 that the autogenerated declarations for autoparams (created by docs#Lean.Elab.Term.declareTacticSyntax) don't respect scoping directly, i.e., they don't start with _private when they "should".

However, they do start with _auto and have macro scopes, so they are not accessible to the user.

Should they also be private per se when appropriate, or is this intended?

I'm basically asking for two reasons: (1) to attempt to be helpful, in case this was overlooked and affects builds somehow (2) to figure out what the right criterion for a "private declaration" really is re: that linter. :)

[Kim Morrison]

@Thomas Murrills, Sebastian is travelling at present, so may not see this message. Could you open a lean4 issue about this?

[Thomas Murrills]

Will do. :) By the way, do you think I should do so for #lean4 > Public recursor can reference private declaration? as well, or is that a known/expected phenomenon?

[Thomas Murrills]

lean4#11569

[Kim Morrison]

Thomas Murrills said:

Will do. :) By the way, do you think I should do so for #lean4 > Public recursor can reference private declaration? as well, or is that a known/expected phenomenon?

I think I've heard someone mention this issue before, but I can't find where, so I think we'll have to wait for Sebastian.

[Michael Rothgang]

@Sebastian Ullrich Thanks a lot for the prompt fix to lean4#11569! Will this change be in the upcoming Lean release (in < a week), or in the next version? Just to understand if adding a band-aid fix to mathlib is useful or not :-)

[Sebastian Ullrich]

upcoming RC!