## Stream: general

### Topic: Lean 4 is going public

#### Gabriel Ebner (Apr 25 2019 at 10:32):

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

#### Patrick Massot (Apr 25 2019 at 10:51):

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 (Apr 25 2019 at 11:08):

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 (Apr 25 2019 at 11:14):

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 (Apr 25 2019 at 11:26):

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

#### Patrick Massot (Apr 25 2019 at 11:27):

what naming convention? Putting a 4 after Lean?

#### Gabriel Ebner (Apr 25 2019 at 12:01):

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 (Apr 25 2019 at 12:19):

whichIsClearlySuperior

#### Johan Commelin (Apr 25 2019 at 12:20):

whichIsClearlyJava

#### Johan Commelin (Apr 25 2019 at 12:21):

give_me_some_room_to_breathe

#### Keeley Hoek (Apr 25 2019 at 12:25):

theNamingConventionIsAmazing

#### Kevin Buzzard (Apr 25 2019 at 12:28):

willSomeoneWriteSomeCodeWhichChangesOldLeanNamingConventionsIntoThisOne? orIsThatSortOfThingImpossibleInPractice?

#### Keeley Hoek (Apr 25 2019 at 12:30):

forWeirdDeclarationsWhichOurHastilyWrittenSwapperProgramDoesn'tRecognise

#### Sebastian Ullrich (Apr 25 2019 at 12:30):

weDidJustThatHackishlyForTheLean4Repo.willBeMuchEasierAndMoreRobustUsingTheFinalLean4.

#### Johan Commelin (Apr 25 2019 at 12:30):

how_will_we_call_our_categories?

#### Johan Commelin (Apr 25 2019 at 12:31):

comm_ring → CommRing

#### Johan Commelin (Apr 25 2019 at 12:31):

maybe we can start snake_casing them

#### Johan Commelin (Apr 25 2019 at 12:31):

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

ℭ𝔬𝔪𝔪ℜ𝔦𝔫𝔤

#### Sebastian Ullrich (Apr 25 2019 at 12:32):

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 (Apr 25 2019 at 12:34):

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

#### Keeley Hoek (Apr 25 2019 at 12:34):

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

#### Johan Commelin (Apr 25 2019 at 12:34):

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

#### Keeley Hoek (Apr 25 2019 at 12:35):

hahaha now that is fancy

#### Johan Commelin (Apr 25 2019 at 12:35):

Some option naming_convention in leanpkg.toml

#### Johan Commelin (Apr 25 2019 at 12:35):

Or namingConvention if you really want

#### Johan Commelin (Apr 25 2019 at 12:35):

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

#### Sebastian Ullrich (Apr 25 2019 at 12:37):

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

#### Keeley Hoek (Apr 25 2019 at 12:37):

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

#### Keeley Hoek (Apr 25 2019 at 12:38):

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 (Apr 25 2019 at 12:52):

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

#### Edward Ayers (Apr 25 2019 at 13:01):

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

#### Patrick Massot (Apr 25 2019 at 13:21):

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

#### Keeley Hoek (Apr 25 2019 at 13:23):

PascalCase camelCase

#### Johan Commelin (Apr 25 2019 at 13:24):

Oooh! So we should blame Blaise!

#### Edward Ayers (Apr 25 2019 at 13:58):

What does &@, mk_borrowed do?

#### Edward Ayers (Apr 25 2019 at 14:20):

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 (Apr 25 2019 at 16:13):

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

#### Patrick Massot (Apr 25 2019 at 16:19):

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 (Apr 25 2019 at 16:21):

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

#### Patrick Massot (Apr 25 2019 at 16:23):

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 (Apr 26 2019 at 03:59):

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 (Apr 26 2019 at 05:06):

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?

No, not yet

#### Kevin Buzzard (Apr 26 2019 at 08:03):

• 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 (Apr 26 2019 at 12:03):

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

#### Keeley Hoek (Apr 26 2019 at 12:15):

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

#### Gabriel Ebner (Apr 26 2019 at 14:03):

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.

#### Koundinya Vajjha (Apr 26 2019 at 22:16):

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 (Apr 26 2019 at 22:23):

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 (Apr 26 2019 at 22:26):

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 (Apr 26 2019 at 22:46):

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

#### Mario Carneiro (Apr 26 2019 at 23:19):

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 (Apr 26 2019 at 23:20):

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 (Apr 26 2019 at 23:22):

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 (Apr 26 2019 at 23:28):

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

#### Mario Carneiro (Apr 26 2019 at 23:29):

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

#### Mario Carneiro (Apr 26 2019 at 23:29):

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

#### Mario Carneiro (Apr 26 2019 at 23:30):

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

#### Mario Carneiro (Apr 26 2019 at 23:31):

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

#### Joe Hendrix (Apr 26 2019 at 23:37):

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 (Apr 26 2019 at 23:39):

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 (Apr 26 2019 at 23:40):

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 (Apr 26 2019 at 23:42):

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

#### Kevin Buzzard (Apr 29 2019 at 10:50):

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 (Apr 29 2019 at 10:52):

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 (Apr 29 2019 at 10:54):

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 (Apr 29 2019 at 11:05):

What Patrick said

#### Joe Hendrix (Apr 29 2019 at 19:07):

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 (Aug 16 2019 at 10:27):

@Mario Carneiro

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

#### Scott Morrison (Aug 17 2019 at 02:08):

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 (Aug 17 2019 at 20:33):

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

#### Jeremy Avigad (Aug 23 2019 at 16:28):

@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 (Aug 24 2019 at 10:35):

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 (Aug 24 2019 at 10:36):

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

#### Sebastian Ullrich (Aug 24 2019 at 11:09):

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

Last updated: May 14 2021 at 06:16 UTC