closures cannot be compacted

Stream: lean4

[Tomas Skrivan]

I encountered internal panic with the error INTERNAL PANIC: closures cannot be compacted. Is the problem that I have PersistentEnvExtension that stores functions?

I want to write a tactic that is user extensible by providing custom meta code. In particular, I have a special pass in the simplifier that checks if the head of an expression is a registered function, e.g. foo, and then calls user provided function simpFoo : (expr : Expr) -> SimpM (Option Step). I store simpFoo inside of PersistentEnvExtension. If it is the problem, how can I circumvent this?

[Jannis Limperg]

Yes, the serialisation to oleans does not support closures. You'll have to find a non-functional representation of the simpFoo functions.

[Kyle Miller]

Maybe you could look at how norm_num accomplishes this? It sounds like you're essentially implementing the same basic framework, since norm_num uses simp pre/post hooks. It might be more complicated since it uses discrimination trees to speed up matching. Here's its environment extension: https://github.com/leanprover-community/mathlib4/blob/e507f376cf8def4d84e636c00c3454f2262fcf71/Mathlib/Tactic/NormNum/Core.lean#L543

NormNumExt is the type of norm num extensions themselves (like your simpFoo)

[Wojciech Nawrocki]

The usual solution is to store the Name of the constant which contains the simpFoo field in the env extension, and then evaluate it at runtime into a value of type Expr -> SimpM (Option Step) by accessing the environment.

[Tomas Skrivan]

Wojciech Nawrocki said:

The usual solution is to store the Name of the constant which contains the simpFoo field in the env extension, and then evaluate it at runtime into a value of type Expr -> SimpM (Option Step) by accessing the environment.

How do you do that?

[Kyle Miller]

In the norm_num code, the Entry type is what's persisted (it's a discrimination tree key, plus the Name of the constant)

[Kyle Miller]

Then this function is used later to turn this constant back into a NormNumExt. See these lines

[Wojciech Nawrocki]

The core function is Environment.evalConstCheck which takes the Name of a constant c : T in the environment, evaluates it, and gives you back a value of type T.

[Tomas Skrivan]

Great, thanks a lot! It is much clearer now and I see the purpose of α and β in the environment extensions.

What is the difference between ScopedEnvExtension and PersistentEnvExtension? Which one should I use? What extra functionality does PersistentEnvExtension provide?

[Wojciech Nawrocki]

Afaict, a ScopedEnvExtension is a PersistentEnvExtension which also handles namespaces, e.g. if you wanted to get the same behaviour as scoped syntax .., you would need a ScopedEnvExtension. But if your custom data is not fine-grained enough to require scoping, maybe just Persistent is fine.

[Wojciech Nawrocki]

You could grep the Lean sources for registerSimpleScopedEnvExtension.

[Mario Carneiro]

ScopedEnvExtensions can have local and scoped declarations, meaning that local entries go out of scope at the end of sections and scoped entries can re-enter the scope using open

[Mario Carneiro]

PersistentEnvExtension are just permanent additions to the env with no provision for erasure

[Tomas Skrivan]

Thanks, makes sense

[Tomas Skrivan]

Again thanks everyone for the help. It works as expected now!