How to change the `#eval` duration?

Stream: new members

[Marko Grdinić]

It times out too quickly for the game I am trying to run it on. I am not expecting much from Lean here, but I want to get a sense how long it takes it to run even a single iteration. In addition to removing timeout is there a way to do #eval with timing included?

[Kevin Buzzard]

If it's a deterministic timeout then you can change the timeout parameter. I think it's -T if you're running Lean from the command line, and in VS Code just search in settings->preferences for lean timeout

[Kevin Buzzard]

And there's always #reduce which is either far quicker or far slower, I can never remember which is which

[Marko Grdinić]

I remember reading that #eval is faster. Also, thanks I'll give it a shot.