Zulip Chat Archive

Stream: Codewars

Topic: Updating Lean support to v3.11.0?


view this post on Zulip Donald Sebastian Leung (May 13 2020 at 06:10):

The current version of Lean used on Codewars is 3.7.2 which is about a month or two behind the newest 3.11.0. I've noticed that some newcomers have encountered issues with conflicting Lean versions between their local installation and the one used on Codewars.

In general, how much of an issue is it for Codewars as a training platform for Lean to use an outdated version of Lean + mathlib like v3.7.2? If a noticeable fraction of the Lean community is turned away from Codewars primarily due to the outdated setup then we could request support for the newest version (3.11.0 at the time of writing) and perhaps update our setup every month or two.

When that happens, we would temporarily have support for two different versions of Lean, e.g. v3.7.2 and v3.110 (+ mathlib), though ideally we would migrate all existing content to v3.11.0 and then remove support for v3.7.2 once that is done.

What do you think? Is it worth the trouble? Vote :+1: if you would like to see Lean v3.11.0 supported on Codewars (+ monthly / bi-monthly version updates) and :-1: otherwise.

view this post on Zulip Markus Himmel (May 13 2020 at 06:14):

I would love to see regular updates to the Lean version. In fact, I have written a kata which I cannot put on Codewars at the moment because the statement requires definitions that were added to mathlib after 3.7.2.

view this post on Zulip Donald Sebastian Leung (May 13 2020 at 08:46):

Codewars/codewars-runner-cli#815

view this post on Zulip Kenny Lau (May 13 2020 at 13:44):

what mathlib version is CW currently using?

view this post on Zulip Kenny Lau (May 13 2020 at 13:45):

found it: ecdb13831d4671eb304c41e78adb5b280c2fc365

view this post on Zulip Donald Sebastian Leung (May 14 2020 at 04:27):

Here is a list of Lean kata that are currently incompatible with 3.11.0 with mathlib (51e2b4c), feel free to update any kata you have authored in the list to make them compatible with 3.11.0 with mathlib (51e2b4c).

See also: Codewars/codewars-runner-cli#815 (comment)

view this post on Zulip Markus Himmel (May 14 2020 at 04:38):

Am I misunderstanding this page, or is it asking to make the same solution compatible with both 3.7.2 and 3.11.0 at the same time?

view this post on Zulip Donald Sebastian Leung (May 14 2020 at 04:45):

Just making it compatible with 3.11.0 would suffice since 3.7.2 support will be removed once all content is updated

view this post on Zulip Markus Himmel (May 14 2020 at 05:01):

So guess I have to wait until 3.11 becomes available in the version dropdown? For some of my kata there is no way to make them compatible with 3.11 but still compile on 3.7.2

view this post on Zulip Donald Sebastian Leung (May 14 2020 at 06:00):

I think keeping a local copy of the 3.11.0-compatible version of each kata would be a good idea until 3.11.0 is released on Codewars.

Don't worry about making your updates backwards-compatible, you don't need to do that

view this post on Zulip Donald Sebastian Leung (May 14 2020 at 06:03):

Donald Sebastian Leung said:

Here is a list of Lean kata that are currently incompatible with 3.11.0 with mathlib (51e2b4c), feel free to update any kata you have authored in the list to make them compatible with 3.11.0 with mathlib (51e2b4c).

See also: Codewars/codewars-runner-cli#815 (comment)

By the way, once you have upgraded each kata to use 3.11.0 and successfully published the changes on Codewars then please don't forget to remove the updated kata from the aforementioned list for bookkeeping purposes (the community wiki should be editable by all).

view this post on Zulip Kenny Lau (May 14 2020 at 06:36):

why does javascript get to have 5 versions?

view this post on Zulip Kenny Lau (May 14 2020 at 06:58):

I don't exactly understand what I'm supposed to do

view this post on Zulip Kenny Lau (May 14 2020 at 06:59):

are you saying that we need to clear the list before we can have 3.11?

view this post on Zulip Kenny Lau (May 14 2020 at 07:00):

or that we need to clear the list right after we have 3.11 so that in the future we can have newer versions?

view this post on Zulip Donald Sebastian Leung (May 14 2020 at 08:07):

are you saying that we need to clear the list before we can have 3.11?

or that we need to clear the list right after we have 3.11 so that in the future we can have newer versions?

I think kazk means the latter. Basically, once we have 3.11 support, we should try to update as much of our existing content to 3.11 ASAP so we can drop 3.7.

why does javascript get to have 5 versions?

Codewars was a big ball of mud until the past 1.5 years or so (when kazk took over the codebase) so it naturally accumulated tons of legacy content in JS and is no longer feasible to update them all, though there have been plans recently to at least try to update some of them and retire others. In contrast, Lean has just been recently supported and we don't have nearly as much content compared to JS / Python / Java or even Haskell so we can afford to update our content regularly and drop support for older versions.

view this post on Zulip Kenny Lau (May 16 2020 at 06:53):

3.11.0 51e2b4c is now available!

view this post on Zulip Donald Sebastian Leung (May 16 2020 at 16:07):

7 Kata left to update, thanks to all of you who have taken the time to update your kata to make them compatible with 3.11.0.

Once we clear this list, Lean support will leave the Beta phase

view this post on Zulip Kevin Buzzard (May 16 2020 at 16:20):

I've just finished a bunch of marking; I'll do mine now if I can figure out what to do

view this post on Zulip Kevin Buzzard (May 16 2020 at 17:05):

:sad: zmodp seems to have disappeared :-/ (not sad to see it go, but it means there's work to do)

view this post on Zulip Bhavik Mehta (May 16 2020 at 17:09):

Both of mine should be done!

view this post on Zulip Johan Commelin (May 16 2020 at 17:57):

Kevin Buzzard said:

:sad: zmodp seems to have disappeared :-/ (not sad to see it go, but it means there's work to do)

Just remove the p and add [fact p.prime] to your hypotheses.

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:08):

lemma eq_iff_modeq_int {n : } {a b : } : (a : zmod n) = b  a  b [ZMOD (n : )] :=
sorry

lemma eq_zero_iff_dvd_int {n : } {a : } : (a : zmod n) = 0  (n : )  a :=
sorry

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:08):

These both seem to have disappeared

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:13):

I don't know how to get domain (zmod p) in the sense that I no longer know how to include the hypothesis that p is prime. There is this fact and the typeclass and I don't really know what I'm doing.

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:14):

I need to go and do other things. I'm sorry, this kata is far harder to fix than I expected

view this post on Zulip Johan Commelin (May 16 2020 at 18:20):

@Kevin Buzzard I understand that you need to do other things, but with

variables (p : nat) [fact p.prime]

you will automatically get a field instance on zmod p.

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:24):

So this is the canonical way to make p a prime now?

view this post on Zulip Johan Commelin (May 16 2020 at 18:29):

Most of the time, yes

view this post on Zulip Kevin Buzzard (May 16 2020 at 18:51):

(deleted)

view this post on Zulip Kevin Buzzard (May 16 2020 at 19:19):

(deleted)

view this post on Zulip Kenny Lau (May 17 2020 at 08:26):

@Donald Sebastian Leung Every group of order 4 is commutative :check_mark:

view this post on Zulip Kevin Buzzard (May 17 2020 at 08:26):

So now five to go?

view this post on Zulip Kenny Lau (May 17 2020 at 08:37):

Sum of Multiples of 3 or 5 Below A Given Number :check_mark:

view this post on Zulip Kenny Lau (May 17 2020 at 08:44):

Order-preserving bijection from rationals to non-zero rationals :check_mark:

view this post on Zulip Donald Sebastian Leung (May 17 2020 at 11:57):

Kevin Buzzard said:

So now five to go?

1 left :wink: "Real Chebyshev" fails to be updated due to timeouts :sad:


Last updated: May 08 2021 at 22:13 UTC