## Stream: new members

#### 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?

#### Scott Morrison (Mar 01 2021 at 23:48):

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

#### Scott Morrison (Mar 01 2021 at 23:48):

In either case the answer is no. :-)

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

#### 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!

#### 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

#### 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

@Rany Tith

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

#### 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