Zulip Chat Archive

Stream: new members

Topic: How to change the `#eval` duration?


Marko Grdinić (Oct 27 2019 at 09:04):

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 (Oct 27 2019 at 09:25):

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 (Oct 27 2019 at 09:26):

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

Marko Grdinić (Oct 27 2019 at 09:30):

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


Last updated: Dec 20 2023 at 11:08 UTC