exact? and apply? high memory usage

Stream: mathlib4

[Newell Jensen]

Using exact? and apply? today was basically hanging my system. I restarted vscode and watched lean eat up my memory each time I used the above commands and it wouldn't release the memory after either finding an answer or me stopping the search. I was able to make it climb and eat all 16 GB on my laptop. To work around this I monitored my memory usage and would restart vscode when it started getting high. I should preface this with I have set_option maxHeartbeats 10000000 set as there was a theorem that needed it. Additionally, I am on mathlib 26b25885bff1060bd207eb45ab1ddf6e534ae6c1 and lean leanprover/lean4:v4.2.0-rc1

[Kyle Miller]

(@Newell Jensen I don't think it's related to the other topic, so I've moved it here)

[Kyle Miller]

Are you able to make a #mwe to reproduce this?

[Newell Jensen]

Let me see. One of the reasons I was just making a passing comment in the other thread is I have moved on from the issue for the time being and my code has changed but I might be able to get it to start eating the memory again.

[Newell Jensen]

It's working great now so I am not sure what was hanging it up before. I do remember I had about 10 haves in the proof (I tend to do this before golfing the code to make sure I am getting things to work step by step before stitching it back together in a more succinct form). Oh well. If I hit it again I will be sure to stop and share an #mwe so as to troubleshoot it.

[Scott Morrison]

Even just a commit pointing to a reproducible state would be helpful for an issue like this (where a #mwe may be too much to ask).