Zulip Chat Archive

Stream: Codewars

Topic: Updating Lean support to v3.11.0?

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.

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.

Donald Sebastian Leung (May 13 2020 at 08:46):

Codewars/codewars-runner-cli#815

Kenny Lau (May 13 2020 at 13:44):

what mathlib version is CW currently using?

Kenny Lau (May 13 2020 at 13:45):

found it: ecdb13831d4671eb304c41e78adb5b280c2fc365

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).

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?

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

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

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

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).

Kenny Lau (May 14 2020 at 06:36):

why does javascript get to have 5 versions?

Kenny Lau (May 14 2020 at 06:58):

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

Kenny Lau (May 14 2020 at 06:59):

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

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?

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.

Kenny Lau (May 16 2020 at 06:53):

3.11.0 51e2b4c is now available!

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

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

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)

Bhavik Mehta (May 16 2020 at 17:09):

Both of mine should be done!

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.

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

Kevin Buzzard (May 16 2020 at 18:08):

These both seem to have disappeared

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.