Move Lean Support out of Beta

[DonaldKellett]

So now we have 76 Lean kata in total (compared to 79 in Coq as reference), 50 of which have been approved and no major issues with the current setup thus far. What do you say about moving Lean out of Beta and officially declaring it as a stable supported language on Codewars?

---

👍 reaction may help

[monadius]

One thing which need to be done before moving Lean out of Beta is to update the mathlib version and see how easy it will be to fix existing kata. I don't know about Lean itself, but mathlib should be periodically updated.

[DonaldKellett]

AFAIK mathlib commits are tightly coupled with the Lean version so we will probably have to update our Lean version as well. I'll ask the community over at Zulip if having a slightly outdated Lean + mathlib (v3.7.2 compared to the current v3.11.x) is an issue, and if so, we can request for the Lean version (and the corresponding mathlib) to be updated.

[monadius]

Lean 3.11 with the updated mathlib is considerably slower than Lean 3.7.2. Because of this, I am not able to update the Lean version of my Chebyshev kata. I created an (almost) empty kumite which demonstrates that just importing analysis.special_functions.trigonometric is enough to get a timeout in Lean 3.11.

[kazk]

:(
I made the container image exactly the same way so I believe Lean 3.11.0 and/or this mathlib version is much slower for some things. Currently 65/81 kata have 3.11.0 enabled (was compatible and also didn't timeout).

If I remember correctly, Lean 3.7 was slower than 3.5 and 3.6 as well (which was also slightly slower than 3.4) when I was experimenting (codewars/codewars-runner-cli#773). I'm not increasing the time limit every time it gets slower.

[DonaldKellett]

For Lean-only kata that cannot be updated due to timeouts, perhaps we should just retire them? Not sure how to handle those with Coq versions as well though (IIRC it cannot just be removed due to database issues?) ...

[monadius]

Let's just wait. If understand this Zulip discussion correctly, long import times is a known issue and it may be fixed in future Lean releases. Although it is also true that mathlib itself is growing and timeouts in future are still possible.

[DonaldKellett]

@kazk All except Real Chebyshev have been updated to 3.11.0.

[kazk]

We can keep 3.7.2 for now. Hopefully, the next update fixes the problem.
I'll close when I deploy the change to move Lean out of beta.

[kazk]

Deployed

[sainiboey]

what is kata

[DonaldKellett]

Thanks for moving Lean out of Beta, I've updated the Wiki to reflect the change. By the way, it seems that the main page still says that Lean is in Beta?

[kazk]

The cache wasn't invalidated. It should be fixed now.