roadmap

Stream: new members

[Rany Tith]

Hi all,

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

[Scott Morrison]

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

[Scott Morrison]

In either case the answer is no. :-)

[Scott Morrison]

(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]

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]

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]

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

[Mario Carneiro]

@Rany Tith

[Mark Gerads]

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

[Bryan Gin-ge Chen]

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.