Is there a faster way to run #eval (MetaM) as executable

Stream: new members

[Nada Amin]

I running into some limitations with stack space using #eval on a MetaM:
libc++abi: terminating due to uncaught exception of type lean::stack_space_exception: deep recursion was detected at 'expression equality test' (potential solution: increase stack space in your system)

I thought that I could try to run the #eval at runtime, but converting from the MetaM to IO so that it can be in main causes issues with import (into the project) when I run lake exe after using TermElabM.toIO.

Is there a best practice to convert from MetaM to IO, and is this a good idea to avoid bottlenecks with #eval?

[Kyle Miller]

Running in IO means setting up the whole Lean environment and importing modules.

Maybe you could instead create a MetaM function in a library that you natively compile then import into the module you want to #eval it?

Do you have some reason to believe that compiling it would relieve deep recursion though? Maybe you need to write your functions differently to not recurse so deeply?

[Nada Amin]

Thanks, debugging further, it seems like I am programmatically trying to run simp on a statement where simp gets stuck. So I'll find a work around for that using a timeout.

I was just wondering about the best practices of running in eval vs running in main, but I infer from your message that if things are not working in eval, they won't magically get better in main.

Thanks, again!