Zulip Chat Archive

Stream: new members

Topic: roadmap


view this post on Zulip Rany Tith (Mar 01 2021 at 23:13):

Hi all,

Apologies if this has been posted somewhere already. Is there a general timeline/roadmap that Lean is following?

view this post on Zulip Scott Morrison (Mar 01 2021 at 23:48):

Do you mean the development of the new language Lean 4, or the mathematics library mathlib?

view this post on Zulip Scott Morrison (Mar 01 2021 at 23:48):

In either case the answer is no. :-)

view this post on Zulip Scott Morrison (Mar 01 2021 at 23:49):

(Presumably Leo and co have some internal roadmaps for Lean 4, but there is not a public one that I'm aware of.)

view this post on Zulip Rany Tith (Mar 02 2021 at 01:05):

Ah okay thank you so much. A public roadmap would be nice as we can be aware what might be deprecated so we don't rely too much on them. For example, the difference between Lean 4 and Lean 3. But to my understanding, Lean does not have an LTS version yet so this might be asking too much. Thanks again!

view this post on Zulip Mario Carneiro (Mar 02 2021 at 03:04):

These deprecations are gradually coming to light, they are generally deprecated as soon as we discover them so we can't say anything about deprecations in advance

view this post on Zulip Mario Carneiro (Mar 02 2021 at 03:05):

A fair number of deprecated things and anti-patterns are encoded in our linter framework, so you should make sure that your code passes that

view this post on Zulip Mario Carneiro (Mar 02 2021 at 03:05):

@Rany Tith

view this post on Zulip Mark Gerads (Mar 02 2021 at 03:38):

How does one lint offline? I thought it might be a leanproject command, but it is not.

view this post on Zulip Bryan Gin-ge Chen (Mar 02 2021 at 03:41):

There are two linters; one of them is written in Lean and can be run by putting #lint at the bottom of the file (or after the declarations you wish to check, see this link for more info.)

The "style linter" is just a python / shell script that you can run with ./scripts/lint-style.sh from the root of mathlib.


Last updated: May 17 2021 at 22:15 UTC