Detect closures before pickling

Stream: lean4

[Thomas Murrills]

To prevent the "closures cannot be compacted" error, I'm wondering if there's a lean-internal way to detect if a given object has closures before attempting to pickle it. E.g. I'd like to be able to write something like

unless ← hasClosures a do pickle "/file/path" a

I'm also a little unclear as to what "closure" is referring to in this context. My understanding of "closure" is, roughly, "unevaluated expression involving variables + variable assignments", but what sorts of variables and assignments are being talked about in this context?

[Joachim Breitner]

I'd assume it's any value of function type.

[Thomas Murrills]

Hmm, it does seem that those give that error, but that's not my understanding of what a "closure" is...

[Thomas Murrills]

Is the actual class of things that can't be serialized broader than things of function type, or does "closure" not mean what I think it means (either in this context or in general)?

[Thomas Murrills]

And, another question, I suppose: how does Lean manage to store e.g. the declaration def foo (x : Nat) := x + 1 in an olean if it can't store objects of function type? (I figure we bypass lean objecthood somehow, but how?)

[Thomas Murrills]

Also: unfortunately simply unfolding the type as much as possible isn't always sufficient for detecting closures, as there's sometimes opacity in the way.

Maybe something like @[extern "lean_is_closure"] after LEAN_EXPORT(?) would work? Though I'm not used to fiddling with C files, and I'd want to have some confidence this makes any sense before I spend time on it :sweat_smile:

[Kyle Miller]

I'd like to be able to write something like

What's the broader context?

[Thomas Murrills]

It's similar to #lean4 > Best way to “compile” an attribute-based function, but a more general case: I need to pickle as much of the environment as I can so that I can look at it elsewhere/later. It would be great to pickle the state of persistent env extensions directly when possible, and indirectly when not. But that requires discriminating based on their picklability—and unless you know the specific env extensions you want to pickle in advance (I don't, this is meant to be generic), it's difficult (impossible?) to access the "true" type of their state, which is hidden behind an opaque EnvExtensionState.

[Kyle Miller]

This doesn't seem like a good direction to go in. Why do you want to conditionally store data in two different ways rather than in a uniform way?

Are you working on something that you can't talk about? Or can you give an outline of your project?

[Thomas Murrills]

Sorry, indeed I'm not allowed to give too many details! :sweat_smile: The main reasons here are performance and fidelity; there is a tradeoff between fidelity and consistency, but that's ok in this case. I suppose it's possible that the nonuniformity will cause a performance hit? But I don't know that yet.