Add Lean 3.16.3 about codewars-runner-cli HOT 6 CLOSED

At first, I thought 2 months have passed already, but it's been only a month. I wrote maybe update every 2 months or so (#815 (comment)). That's already a lot more frequent than other languages.

But if it's really that much faster, then I'll consider making this an exception so that we can remove the old version.

from codewars-runner-cli.

But if it's really that much faster, then I'll consider making this an exception so that we can remove the old version.

Yeah, they have a new minor version every week and mathlib is ever evolving (-:

from codewars-runner-cli.

? I meant faster as in performance and not how fast (frequent) they release.

Can someone compare the performance of Real Chebyshev?

Also posting leanpkg.toml here would help.

from codewars-runner-cli.

I just tried submitting https://www.codewars.com/kata/5ea1f341014f0c0001ec7c5e/ with no code in it at all. Just import Preloaded fails with "Execution Timed Out (20000 ms)". The kata is unsolveable.

I'm not sure upgrading Lean will help, but it takes about 2 seconds to check my solution locally (on a laptop, not a particularly fast machine).

from codewars-runner-cli.

@jorendorff Uniqueness of limits in a metric space is indeed very close to the timeout limit in 3.11.0. If you have a working solution to it locally then try re-submitting your solution on Codewars until it passes. From my previous experience trying to upgrade the kata to 3.11.0 it works maybe about 1 in 10 times.

from codewars-runner-cli.

Closing in favor of #828

from codewars-runner-cli.