Stream: new members
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: May 12 2021 at 05:19 UTC