Extending the timeout limit for Lean

[DonaldKellett]

So @kbuzzard just recently came up with a very difficult Lean Kata (difficult math + performance requirements) to be published on Codewars which runs in about 10s on his local machine but runs in about 40s on mine and consistently times out on Codewars' servers. Based on my experience, Codewars' servers take about 2 / 3 of the time it takes on my machine to execute so I suspect it should take about 25-30s.

@kazk Would it be possible to extend the time limit for Lean on Codewars, to, e.g. 20s or even 30s? I have sent you his Kata setup by email for your reference, and here are the cumulative profiling stats on my local machine for that Kata idea:

cumulative profiling times:
    compilation 0.432ms
    decl post-processing 2.05ms
    elaboration 17.8s
    elaboration: tactic compilation 174ms
    elaboration: tactic execution 15.4s
    parsing 6.47s
    type checking 1.88ms

[DonaldKellett]

Any updates on this? IMO extending it to 20 seconds would be ideal, though extending it beyond that would probably hold up resources for too long.

[monadius]

I support the idea of increasing Lean's timeout to 20 seconds. Imports take a lot of time. For example, import analysis.complex.exponential requires 14.5 seconds (when I tried this import several days ago, it was about 15.5 seconds).

[kazk]

20s should be fine.

[kazk]

Done

[monadius]

I still get 16 second timeouts in Lean. I created a Lean translation of my Chebyshev polynomial kata (link to my translation draft). But I get Execution Timed Out (16000 ms) when I try to run it.

[kazk]

Sorry, it looks like I had cut the release just before the commit that extended Lean time limit. I just deployed a new release including it.

[monadius]

Thank you @kazk! Everything works now and I was able to publish my translation.