private access

Stream: lean4

[Joseph O]

If I mark a function private, can it only be accessed within that namespace or section and nowhere else, or is it not that strict?

[Simon Hudon]

Those declarations are still in the environment after the namespace is closed but its name is mangled. If you defined it as Namespace.foo and defined it in dir/file.lean, it will be in your environment as dir.file.0.Namespace.foo (or with another number if there are multiple private definitions with the same name in the same file).

[Gabriel Ebner]

If you're using mathlib4, you can also do open my.private.defn from Module.Where.Its.Defined.In to comfortably access private definitions from other modules.

[Adam Topaz]

What's the current preferred way to open a private definition? Is the above still valid? I couldn't get it to work.

[Adam Topaz]

Okay, I figured it out, it's open private name from module

[Johan Commelin]

Oof, why do you need access to a private defn? That seems like a code smell to me?

[Johan Commelin]

Is there some API that is incomplete?

[Adam Topaz]

I need a bounded variant of docs#Lean.Meta.lambdaLetTelescope and the implementation of this has such an option, but is marked as private.

[Adam Topaz]

This is for a private project unrelated to mathlib etc. so I'm not too worried about using private defs

[Adam Topaz]

Note that we do have docs#Lean.Meta.lambdaBoundedTelescope but not something that will also handle letE exprs.

[Jannis Limperg]

The Lean API has a bunch of private functions that are generally useful (and are no more dangerous than many public functions).

[Johan Commelin]

Hmm, is there a list of some examples? It would be good to record them in some place. Because I think this just needs fixing.

[Adam Topaz]

FWIW, the private def that I needed is this one

[Jannis Limperg]

Johan Commelin said:

Hmm, is there a list of some examples? It would be good to record them in some place. Because I think this just needs fixing.

If core agrees that this is a good idea, the best thing to do would be to just start sending PRs. But I'm not sure core agrees; API improvements that aren't bug fixes don't seem to be a high priority (understandably, given that we can usually work around them).

[Kim Morrison]

There is tension here:

• keeping things private means we can change the implementation without worrying about compatibility: it adds cost to us to make things public
• sometimes people have good uses cases downstream that depend on the implementation: and we end up sad that open private is being used, and we are being pushed into supporting an implementation detail.

[Kim Morrison]

I think we are open to making some private things public. But it should go through the RFC process, rather than starting with a PR. The RFC should

• explain the use case downstream
• point to evidence that it is necessary for a significant project (<---)
• explain why it is not possible to use the public API to achieve that effect
• if there are any relevant suggestions about changing the API as we make it public, make those

[Kim Morrison]

Doing a first round of prioritisation here on zulip would be even better. If someone could identify the current uses of open private that Mathlib most heavily depends on having, that would be a great way to triage work in this direction.

[Mario Carneiro]

One reason open private is better than copy paste is that the upstream version changes too instead of having slight variations on the same code promulgate

[Mario Carneiro]

we are being pushed into supporting an implementation detail

I don't think anyone is advocating for that. Using open private is voiding your warranty, I don't think anyone thinks otherwise

[Kim Morrison]

I regularly have to fix code adjacent to an open private. Warranty might be voided, but it's often still my problem. :-) Outside of Batteries/Mathlib, sure, go wild.

[Mario Carneiro]

Kim Morrison said:

I think we are open to making some private things public. But it should go through the RFC process, rather than starting with a PR. The RFC should

• explain the use case downstream
• point to evidence that it is necessary for a significant project (<---)
• explain why it is not possible to use the public API to achieve that effect
• if there are any relevant suggestions about changing the API as we make it public, make those

The trouble is that this is an extremely heavyweight process given that there are hundreds or thousands of private definitions in Lean. I can't imagine any scenario where it would be worth it. If it was just a matter of recording when, where and why open private is being used in downstream projects, that is reasonable, but open private is a conflict avoidance method, and writing an RFC is not.

[Kim Morrison]

Mario Carneiro said:

One reason open private is better than copy paste is that if the upstream version changes too instead of having slight variations on the same code promulgate

Definitely agree on this one. Fixing subtle ancient variations of the internals of simp copy-pasted into downstream projects is not fun.

[Kim Morrison]

100s or 1000s is a straw man. I'm talking about open private on the critical path to Mathlib, and I think there's more like half a dozen.

[Mario Carneiro]

the list evolves regularly, and it is difficult to predict what will be on it

[Mario Carneiro]

I think batteries is currently open private-free?

[Mario Carneiro]

I should grep rather than guess

[Kim Morrison]

2 in batteries, 1 in aesop

[Kim Morrison]

so half a dozen was an overestimate

[Mario Carneiro]

Batteries:

open private mkMetaContext from Lean.Elab.Command
open private preprocess from Lean.Meta.Tactic.Simp.SimpTheorems

Mathlib:

open private getElimNameInfo generalizeTargets generalizeVars from Lean.Elab.Tactic.Induction
open private getIntrosSize from Lean.Meta.Tactic.Intro
open private Simp.dischargeUsingAssumption? from Lean.Meta.Tactic.Simp.Rewrite
open private withFreshCache mkAuxMVarType from Lean.MetavarContext

[Kim Morrison]

The one in Aesop is getIntrosSize again

[Mario Carneiro]

is there more information you need besides the function names? I can try to reconstruct why these functions are being used, but a common reason is that these are the functions one level below an entry point function and we need to modify the entry point behavior

[Mario Carneiro]

also of note is that my test file contains 11 open privates. When debugging lean code it is very useful to be able to inline lean functions and this means you have to be able to open private to copy the function body

[Kim Morrison]

No complaints about test files using it!

[Mario Carneiro]

mkMetaContext is a bit embarrassing, you can't create a CommandElabM state without it

[Mario Carneiro]

well, you could copy paste the list of settings in that object, but it's basically a config struct with default settings, you can imagine the nightmare if that gets out of date

[Mario Carneiro]

I think there is already an issue which suggests that those settings should be the default values so that {} works

[Mario Carneiro]

currently there is an issue where depending on how you run a command (i.e. which entry point) you can end up running it with either mkMetaContext or {} as the setting, which affects some extremely obsure elaboration details. Debugging that one was not fun