Zulip Chat Archive

Stream: general

Topic: give #eval more time

Chris Hughes (Sep 09 2018 at 15:42):

Is there a way to give #eval more time before a deterministic timeout?

Kevin Buzzard (Sep 09 2018 at 15:45):

On the command line there is a --timeout=num option.

Kevin Buzzard (Sep 09 2018 at 15:46):

So I guess you could try editing your VS Code preferences (if you want to do this in VS Code)

Kevin Buzzard (Sep 09 2018 at 15:46):

wooah Ctrl-comma in VS Code has changed.

Kevin Buzzard (Sep 09 2018 at 15:48):

oh actually I've just found that it is an option in VS Code: 

  // Set a deterministic timeout (it is approximately the maximum number of memory allocations in thousands) for the Lean server.
  "lean.timeLimit": 100000

So try ctrl-comma (or file -> preferences -> settings) and then search for lean.timeLimit and try changing that (maybe you have to click on a pencil and say you want to edit it before you can edit it)

Kevin Buzzard (Sep 09 2018 at 15:49):

I only half-know what I'm talking about here though, so no guarantee of success.

Chris Hughes (Sep 09 2018 at 15:54):

Doesn't seem to make any difference.

Keeley Hoek (Sep 09 2018 at 15:55):

did you restart the lean server after you did it? I forget this more often than I'd like...

Chris Hughes (Sep 09 2018 at 16:08):

No I didn't. Thanks @Keeley Hoek

Chris Hughes (Sep 09 2018 at 16:18):

Thanks. I have now managed to compute that my proof of quadratic reciprocity used exactly 5000 theorems, definitions, axioms and constants traced all the way back to axioms.

Bryan Gin-ge Chen (Sep 09 2018 at 16:50):

That's cool! Have you posted the script for doing that somewhere?

Last updated: Dec 20 2023 at 11:08 UTC