Adding Lean support to Codewars

Stream: general

[Donald Sebastian Leung]

Hello there! The Codewars community has recently been pondering about adding Lean support to Codewars, which is a recreational/competitive programming OJ website and probably the only one that currently supports theorem-proving languages (currently Coq, Idris and Agda) to any meaningful extent.

Seeing as the last stable version of Lean 3 has been released and Lean 4 development is well underway, I would like to ask the following questions:

• How long until the first beta/stable version of Lean 4 is officially released?
• Once Lean 4 is officially released, how long before Lean 3 will be (more-or-less) completely phased out?
• To what extent will backwards compatibility be broken between Lean 3 and Lean 4? Will it be that only certain Lean 3 projects relying on advanced Lean features be broken in Lean 4, or will even the simplest Lean 3 project (e.g. on the scale of one of the levels of the natural number game) possibly no longer compile under Lean 4?
• Therefore, if Lean support were to be added to Codewars in the near future, is Lean 3 or Lean 4 a better choice, or is it better not to add Lean at all?

For your reference, here is the issue ticket for requesting Lean support on Codewars - if you are interested in this, please do leave a :+1: on the issue to show your support :smile:

[Johan Commelin]

@Donald Sebastian Leung Welcome!

• Lean 4: there's no official statement. It'll be done when it's done. Our guesses are: maybe late this year, maybe beginning of next year. The only thing that has been said is that it will be in 201X, and we now know that X ≥ 10.
• Phasing out of Lean 3: We are currently transitioning to Lean 3.5.c, a version that is maintained by the community. So we might start "phasing out" Lean 3.4.2 pretty soon. This move isn't too drastic. The move to Lean 4 will take a lot more time. Again, no official statements. We'll be done with the migration of mathlib once we're done.
• Backwards compatibility: This will be broken pretty seriously. On the other hand, the parser in Lean 4 will be so flexible that people have suggested writing a Lean 3 parser-frontend for Lean 4. So it might not be a very big problem.
• Choice: If have no idea how hard it is to add a language. But I think that with Lean 3 you could have fun for at least another 2 years. With Lean 4 you will have a serious programming language if you use the current version from the development repo, but you will not have any proving environment, because the tactic framework isn't there yet. Also it isn't stable, so thing may break on an update.

My advise would be to go with Lean 3.5.c, and then see if you want to move to Lean 4 some two years from now. But it's good to also hear what others think.

[Yury G. Kudryashov]

(deleted, @Johan Commelin wrote it better)

[Donald Sebastian Leung]

Johan Commelin said:

Donald Sebastian Leung Welcome!

• Lean 4: there's no official statement. It'll be done when it's done. Our guesses are: maybe late this year, maybe beginning of next year. The only thing that has been said is that it will be in 201X, and we now know that X ≥ 10.
• Phasing out of Lean 3: We are currently transitioning to Lean 3.5.c, a version that is maintained by the community. So we might start "phasing out" Lean 3.4.2 pretty soon. This move isn't too drastic. The move to Lean 4 will take a lot more time. Again, no official statements. We'll be done with the migration of mathlib once we're done.
• Backwards compatibility: This will be broken pretty seriously. On the other hand, the parser in Lean 4 will be so flexible that people have suggested writing a Lean 3 parser-frontend for Lean 4. So it might not be a very big problem.
• Choice: If have no idea how hard it is to add a language. But I think that with Lean 3 you could have fun for at least another 2 years. With Lean 4 you will have a serious programming language if you use the current version from the development repo, but you will not have any proving environment, because the tactic framework isn't there yet. Also it isn't stable, so thing may break on an update.

My advise would be to go with Lean 3.5.c, and then see if you want to move to Lean 4 some two years from now. But it's good to also hear what others think.

Thanks @Johan Commelin for your input, I will make a note of Lean v3.5.c on the issue ticket. BTW is Lean v3.5.c out yet, and if so, where can I find it?

[Bryan Gin-ge Chen]

Lean 3.5.1 (and future community-maintained releases of Lean 3) can be found at https://github.com/leanprover-community/lean

[Scott Morrison]

(Aside: lets just stop using the 'c' modifier in version numbers. It's just 3.5.1, and we can note somewhere that 3.4 --> 3.5 was the transition to the "community" version.)

[Mario Carneiro]

I think the intent is something of a "warranty free" clause for microsoft's benefit. Lean 3.5 is not affiliated with microsoft, 3.4 is

[Patrick Massot]

I think Leo is careful to keep the distinction between what comes from his work (and the work of his team) from the community effort. It doesn't cost much to respect that by putting that little c.

[Patrick Massot]

About the original question: I think people at codewars should try to have a Lean3 support (including the 3 in the name). They could also have Lean4 support already, especially for this kind of challenge, but it should be considered as a different language. Nothing will be compatible out of the box.

[Donald Sebastian Leung]

Patrick Massot said:

About the original question: I think people at codewars should try to have a Lean3 support (including the 3 in the name). They could also have Lean4 support already, especially for this kind of challenge, but it should be considered as a different language. Nothing will be compatible out of the box.

Noted, thanks for bringing this up. Maybe I will edit the title of my issue ticket to reflect this.

[Patrick Massot]

Maybe I should expand a bit on my comment. Lean4 is already available. It is already usable by programmers, a couple of them are currently writing a very non-trivial program using mostly that language (they are writing Lean 4 itself using Lean 4). The reason mathematicians like me don't use it yet is that it's not yet usable as an interactive theorem prover. So you could already have coding challenges using Lean 4, although you would probably have trouble finding good documentation.

[Donald Sebastian Leung]

Hi there, it appears that we're encountering a serious performance issue when compiling user solutions with our current setup which is preventing us from releasing Lean support on Codewars. For example, a simple proof of 0.999... = 1 I wrote that runs in about 8 seconds on @Kevin Buzzard 's machine is taking 50 seconds on our servers, even though we've included the nightly .olean files for mathlib as far as I can tell. If anyone could take a closer look at our current environment setup and perhaps tell us what we're doing wrong which is causing the compilation times to be much longer than necessary then that would be great.

Many thanks for your help and attention! :smile:

[Mario Carneiro]

From your script it looks like you aren't touching the olean files, so they might be getting ignored

[Kevin Buzzard]

The timestamps of each olean file has to be later than that of the corresponding lean file

[Donald Sebastian Leung]

Mario Carneiro said:

From your script it looks like you aren't touching the olean files, so they might be getting ignored

Thanks @Mario Carneiro , would you mind elaborating? Does that mean that running touch someFile.olean for every .olean file in mathlib will solve the issue?

Kevin Buzzard said:

The timestamps of each olean file has to be later than that of the corresponding lean file

Thanks, I will mention this in my GitHub issue ticket.

[Rob Lewis]

The incantation I usually use (provided by someone else here) is find _target | grep "[.]olean$" | xargs touch. This should give each olean file the same current time stamp. You need that (1) one.olean is at least as recent as one.lean and (2) if two.lean imports one.lean then two.olean is at least as recent as one.olean.

[Rob Lewis]

There's infrastructure coming very soon that should handle all of this olean fetching for you, if you have Python in your environment. https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/new.20mathlib.20tools

[Donald Sebastian Leung]

As it currently stands, Codewars will need to upgrade its servers (which probably won't happen anytime soon) in order to reasonably support Lean challenges of nontrivial complexity, thank you for everyone's support over the past two weeks.

[Sebastian Ullrich]

@Donald Sebastian Leung It's a bit disappointing that Coq+mathcomp would be fast enough for Codewars, but Lean+mathlib would not. I see in the Coq PR that you all decided not to use coqchk because it was too slow, so it would be great to have a reliable Lean verify script that does not need leanchecker either. Perhaps a nice-to-have for Lean 3.7.0? /cc @Gabriel Ebner @Kevin Kappelmann

[Donald Sebastian Leung]

Sebastian Ullrich said:

Donald Sebastian Leung It's a bit disappointing that Coq+mathcomp would be fast enough for Codewars, but Lean+mathlib would not. I see in the Coq PR that you all decided not to use coqchk because it was too slow, so it would be great to have a reliable Lean verify script that does not need leanchecker either. Perhaps a nice-to-have for Lean 3.7.0? /cc Gabriel Ebner Kevin Kappelmann

I don't think it would be fair (for Lean) to compare Coq and Lean (in terms of Codewars support) based on mathcomp/mathlib since the vast majority of Coq challenges on Codewars focus on CS topics such as PL theory and algorithmic verification as opposed to "fashionable mathematics" and therefore rarely use mathcomp at all. I think the only two Coq challenges on the site (out of 46 approved and 60+ total) that use mathcomp to any extent are Real Fibonacci and Real Chebyshev.

[Johan Commelin]

Well, we don't really have fashionable maths in mathlib yet either