Zulip Chat Archive

Stream: general

Topic: question about the future of lean 3


view this post on Zulip Gun Pinyo (Jul 19 2020 at 08:59):

Lean 3 is still the recommend version of lean, due to fact that lean 4 is still under the development.
I am sure that lean 4 will bring many improvements over lean 3. However, once lean 4 is official released. Is the lean 3 still being maintain?

I am asking this because someone might still want to use lean 3 because of legacy reason or syntax convention (I like snake case more, easier to read).
I know this is lame, but sorry the camel case really sore and confuse my eyes. Anyway, I also would like to ask why lean 4 changes the naming convention from snake case to camel case? Is it because of fewer space required?

view this post on Zulip Kevin Buzzard (Jul 19 2020 at 09:23):

Probably the future of lean 3 will depend very much on how quickly the community is able to bring lean 4 up to the level of lean 3. Whilst some of us are optimistic that this process will happen quickly, in practice we just have to wait and see.

view this post on Zulip Kevin Buzzard (Jul 19 2020 at 09:25):

By up to the level, I personally mean how quickly we can get the maths library up and running. By the time it becomes feasible to do mathematics like manifolds in lean 4 in a nice and natural way, I can't imagine there will be much enthusiasm for supporting lean 3

view this post on Zulip Kevin Buzzard (Jul 19 2020 at 09:25):

But how long this will take is right now anybody's guess

view this post on Zulip Scott Morrison (Jul 19 2020 at 11:28):

weveGotOurWorkCutOutForUs


Last updated: May 12 2021 at 23:13 UTC