Lean 4 is going public

Stream: general

[Gabriel Ebner]

16 hours ago Leo made the lean4 repo public: https://github.com/leanprover/lean4/

[Patrick Massot]

Wow! Did you receive any kind of announcement? Do we have instructions about things we could test? I wouldn't try anything without being asked to do it.

[Gabriel Ebner]

It just showed up on my github activity feed today. I think the README is pretty clear: "We strongly suggest you use Lean 3."

[Patrick Massot]

I understand the README, what I don't understand is why making it public if there is nothing anyone should do (besides Leo and Sebastian of course)?

[Gabriel Ebner]

The reason is of course to get you used to the new naming convention. :smiley:

[Patrick Massot]

what naming convention? Putting a 4 after Lean?

[Gabriel Ebner]

I'm talking about the namingConvention:

protected theorem mulLtMulOfPosLeft {n m k : Nat} (h : n < m) (hk : k > 0) : k * n < k * m :=
Nat.ltOfLtOfLe (Nat.addLtAddLeft hk _) (Nat.mulSucc k n ▸ Nat.mulLeMulLeft k (succLeOfLt h))

[Sebastian Ullrich]

whichIsClearlySuperior

[Johan Commelin]

whichIsClearlyJava

[Johan Commelin]

give_me_some_room_to_breathe

[Keeley Hoek]

theNamingConventionIsAmazing

[Kevin Buzzard]

willSomeoneWriteSomeCodeWhichChangesOldLeanNamingConventionsIntoThisOne? orIsThatSortOfThingImpossibleInPractice?

[Keeley Hoek]

itIsDefinitelyVeryScriptableMaybeWithAHumanAddressableNumberOfExceptions

[Keeley Hoek]

forWeirdDeclarationsWhichOurHastilyWrittenSwapperProgramDoesn'tRecognise

[Sebastian Ullrich]

weDidJustThatHackishlyForTheLean4Repo.willBeMuchEasierAndMoreRobustUsingTheFinalLean4.

[Johan Commelin]

how_will_we_call_our_categories?

[Johan Commelin]

comm_ring → CommRing

[Johan Commelin]

maybe we can start snake_casing them

[Johan Commelin]

that would make me a very big proponent of bundling everything (-;

[Gabriel Ebner]

ℭ𝔬𝔪𝔪ℜ𝔦𝔫𝔤

[Sebastian Ullrich]

personally_forLemmas_I_wouldSuggest_something_like_theMathematicalComponentsConvention https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md#names-in-the-library-usually-obey-one-of-following-the-convention

[Johan Commelin]

Oh no! Not the 1-letter abbreviations... that makes things even more incomprehensible

[Keeley Hoek]

Yeah no those abbreviations are the worst thing I've ever seen in my life

[Johan Commelin]

Can't we have several user modes, that transparently switch between the naming conventions?

[Keeley Hoek]

hahaha now that is fancy

[Johan Commelin]

Some option naming_convention in leanpkg.toml

[Johan Commelin]

Or namingConvention if you really want

[Johan Commelin]

And then all your dependencies automatically show in your naming convention when you browse the code in VScode

[Sebastian Ullrich]

Oh, I was only referring to their :snake:/:camel: convention. Those abbreviations do look horrible.

[Keeley Hoek]

Leo has almost 6 million LOC changed in the repository history!

[Keeley Hoek]

Sebastian, (obligatory disclaimer: I have literally no expectations please no-one get angry I'm just keen is all) is there any juicy code generation business going on in leanprover/lean4?

[Sebastian Ullrich]

The compiler is there and it's functional and pretty fast, if that's what you're asking

[Edward Ayers]

It looks like the bytecode VM is still there. Is it still hooked up to something or is it vestigial?

[Patrick Massot]

This CamelCase is so awful, I understand you made the repository secret for so long

[Keeley Hoek]

PascalCase camelCase

[Johan Commelin]

Oooh! So we should blame Blaise!

[Edward Ayers]

What does &@, mk_borrowed do?

[Edward Ayers]

To answer my own question: If I am not mistaken it is an optimisation that doesn't copy the argument. Eg in list.length, the output number doesn't need a memory reference to the input list, wheras list.cons does.

[Simon Hudon]

What's the reason for switching the naming convention, by the way?

[Patrick Massot]

I'm sure it's preparing ground for a parser demo: soon they will showcase three lines of Lean asking the parser to rewrite all files using the normal name convention.

[Simon Hudon]

haha! That would be a pretty round about way to do it

[Patrick Massot]

I feel sorry I'm not commenting anything else, I totally lack expertise to write useful comments. But I'm still very happy to see Leo and Sebastian seem to be happy enough about their progress to make it public!

[Mario Carneiro]

I'm still a bit confused about @&. Does lean have a linear type system now?

constant hugeFuel : Nat := 10000

I wonder what constants with definitions means

[Mario Carneiro]

A few more notes to self about new stuff:

• meta has been renamed unsafe (good idea)
• @[macroInline]?
• we have a lot of extern cpp now, I'm curious how that works.
• == now means boolean equals instead of Heq (which has taken both notations ≅ and ~=)
• drec seems to have grown an n (i.e. Eq.ndrec), I'm not sure what it stands for
• @[inlineIfReduce, nospecialize] def Decidable.toBool (p : Prop) [h : Decidable p] : Bool: oh boy, new attributes
• Array is the new name for buffer, array seems to be gone. They are implemented as array lists instead of persistent arrays now (+1 from me)

partial def shrink : Array α → Nat → Array α
| a n := if n ≥ a.size then a else shrink a.pop n

• Oh wow, built in partial definitions! I will have to see how this interacts with the type system
• Everything is Bool now instead of Prop. Not sure how this will interact with pure mathematics stuff
• Expr is non-meta! Woohoo!
• I think tactic is also non-meta, and has been renamed ElaboratorM
• https://github.com/leanprover/lean4/blob/master/library/init/lean/compiler/ir.lean#L10-L11 @Sebastian Ullrich Is the article "Counting Immutable Beans" available anywhere?

[Sebastian Ullrich]

No, not yet

[Kevin Buzzard]

• Everything is Bool now instead of Prop. Not sure how this will interact with pure mathematics stuff

Can you elaborate? Did we become Isabelle?

[Patrick Massot]

Yes, I'm very frightened by this comment. Can anyone explain this?

[Keeley Hoek]

There still literally is a definition notation `Prop` := Sort 0 in init/core.lean

[Gabriel Ebner]

AFAICT, the main difference is that functions such as list.filter no longer takes a decidable predicate as argument, but a function α → Bool. Also lots of stuff uses HasBeq (lawless function α → α → Bool) instead of DecidableEq, but I believe that is just because derive DecidableEq doesn't work yet.

[Kenny Lau]

[Koundinya Vajjha]

partial def shrink : Array α → Nat → Array α
| a n := if n ≥ a.size then a else shrink a.pop n

• Oh wow, built in partial definitions! I will have to see how this interacts with the type system

What are partial definitions?

[Mario Carneiro]

that's a good question. At a glance, I would say it's the analogue of meta that allows non-well founded recursions

[Mario Carneiro]

There are some things you can say about partial definitions that is a little stronger than meta. In particular, although there are obviously partial proofs of false, there is a non-meta notion of "domain" of a partial function, and you can extract a real value from a partial function within its domain. But that's just wishful thinking; probably this is just a viral marker like meta and you don't have direct access to the domain predicate

[Joe Hendrix]

Partial functions require that Lean can show the result type is inhabited; I don't think meta requires that.

[Mario Carneiro]

Not necessarily. A partial function from A to B is really a function from A to (optional B) for some sense of "optional", and so it is always inhabited (by bottom)

[Mario Carneiro]

If lean gets native support for partial functions and definitions, then I imagine it will act something like Haskell's "bottom" value inhabiting all (partial) types

[Mario Carneiro]

This isn't really a new feature - lean 3 meta allows you to write nonterminating computations already - but the separation of meta into partial (meaning unqualified recursion is okay) and unsafe (meaning you are doing something not necessarily sound with the VM representation) seems like a good idea

[Joe Hendrix]

You may be right. I'm just speaking from what I've seen trying out Lean 4.

[Mario Carneiro]

oh, are you saying that the lean 4 typechecker is asking for a proof of inhabited?

[Mario Carneiro]

that's pretty weird if so, because it can't ever use that value

[Mario Carneiro]

I guess it's a low tech way to avoid inconsistency, but it is not maximally expressive

[Mario Carneiro]

I haven't actually tried to run lean 4 yet, I'm just reading the code

[Joe Hendrix]

I've only done a bit of programming, but found it useful so far. I found it tedious to use combinator-based parsers in Lean 3, but the result types of a parser are pretty much always inhabited. I haven't tried out proving things though.

[Mario Carneiro]

My first impression is that lean 4 has skewed a lot more towards programming, possibly at the expense of mathematics. We will have to see

[Mario Carneiro]

Of course the lack of a tactic framework means we won't be porting mathlib any time soon... although possibly lean 4 allows us to write our own tactic framework now?

[Mario Carneiro]

Isn't the lean 4 parser also combinator based? It looks like they built on Haskell's Parsec library

[Kevin Buzzard]

My first impression is that lean 4 has skewed a lot more towards programming, possibly at the expense of mathematics. We will have to see

I have now been assured by the devs that Lean 4 will support mathematics just as well as Lean 3, if not better. I have also been reminded that Lean 4 currently has no tactic framework, so don't anyone get any ideas about porting anything yet :-)

[Kevin Buzzard]

I've only done a bit of programming, but found it useful so far. I found it tedious to use combinator-based parsers in Lean 3, but the result types of a parser are pretty much always inhabited. I haven't tried out proving things though.

@Joe Hendrix could you explain how you're doing this? Do you compile Lean, and then make .lean files using term mode and then run them through lean --make?

[Patrick Massot]

About these rumors, what I think is: because Leo and Sebastian want to rebuild a lot of things in Lean using the Lean programming language, they first focused on the programming aspect. I doesn't mean we won't be able to do math. They need the programming aspects in order to allow rebuilding the tactic framework. Once we get the tactic framework we can start on math

[Sebastian Ullrich]

What Patrick said

[Joe Hendrix]

I just used the command line for trying things out. It's a little clunky at the moment, but I imagine it will be similar to the Lean 3 experience once it makes sense to get leanpkg and the editor interfaces properly working.

[Sebastian Ullrich]

@Mario Carneiro

• https://github.com/leanprover/lean4/blob/master/library/init/lean/compiler/ir.lean#L10-L11 Sebastian Ullrich Is the article "Counting Immutable Beans" available anywhere?

Preprint now available at https://arxiv.org/abs/1908.05647

[Scott Morrison]

My inner editor can't resist noting some typos on page 1.

• last line has a bad overflow
• "where reported here" seems garbled
• "users can extend Lean using Lean itself" needs a capital letter

[Sebastian Ullrich]

@Scott Morrison Thanks, two sentences got merged there. The overflows are on arxiv, no idea what it's doing

[Jeremy Avigad]

@Sebastian Ullrich I have read enough of the paper so far to ascertain that (a) the Lean 4 IR is amazing and that (b) the two of you have done a tremendous amount of hard work. Many thanks to you and Leo for your efforts.

[Sebastian Ullrich]

Thanks, Jeremy! Here's hoping it will reduce the number of times someone complains about their tactic being too slow, haha. Definitely looking forward to what you all will come up with.

[Patrick Massot]

That will depend on how much API documentation you'll write...

[Sebastian Ullrich]

I thought it would write itself, like in the Lean 3 fork