inline affecting whnf

Stream: lean4

[Tomas Skrivan]

Does inline attribute affect how is a function handled by whnf? If I mark a particular function with inline I get whnf heartbeat error.

I would like to have a function that is inlined but not unfolded when typechecking or calling isDefEq. How should I mark such function?

[Kyle Miller]

Could you make a mwe for this? Do you know where in the pipeline the whnf is being done?

I don't think whnf itself knows about the inline attribute, but maybe during compilation inlining sets up a situation that causes whnf to time out?

[Tomas Skrivan]

I didn't have success minimizing it yet. It happens after layers and layers of abstraction and set_option trace.Meta.whnf true does not output anything.

[Tomas Skrivan]

And it is even more compilcated, I have two functions that I want to mark inline as they both have a big impact on performance. I can set only one but not both at the same time.

[Tomas Skrivan]

But I will try to investigate more and hopefully minimize