Zulip Chat Archive

Stream: general

Topic: Lean 4 is going public


view this post on Zulip Gabriel Ebner (Apr 25 2019 at 10:32):

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

view this post on Zulip 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.

view this post on Zulip 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."

view this post on Zulip 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)?

view this post on Zulip Gabriel Ebner (Apr 25 2019 at 11:26):

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

view this post on Zulip Patrick Massot (Apr 25 2019 at 11:27):

what naming convention? Putting a 4 after Lean?

view this post on Zulip Gabriel Ebner (Apr 25 2019 at 12:01):

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

view this post on Zulip Sebastian Ullrich (Apr 25 2019 at 12:19):

whichIsClearlySuperior

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:20):

whichIsClearlyJava

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:21):

give_me_some_room_to_breathe

view this post on Zulip Keeley Hoek (Apr 25 2019 at 12:25):

theNamingConventionIsAmazing

view this post on Zulip Kevin Buzzard (Apr 25 2019 at 12:28):

willSomeoneWriteSomeCodeWhichChangesOldLeanNamingConventionsIntoThisOne? orIsThatSortOfThingImpossibleInPractice?

view this post on Zulip Keeley Hoek (Apr 25 2019 at 12:29):

itIsDefinitelyVeryScriptableMaybeWithAHumanAddressableNumberOfExceptions

view this post on Zulip Keeley Hoek (Apr 25 2019 at 12:30):

forWeirdDeclarationsWhichOurHastilyWrittenSwapperProgramDoesn'tRecognise

view this post on Zulip Sebastian Ullrich (Apr 25 2019 at 12:30):

weDidJustThatHackishlyForTheLean4Repo.willBeMuchEasierAndMoreRobustUsingTheFinalLean4.

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:30):

how_will_we_call_our_categories?

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:31):

comm_ring → CommRing

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:31):

maybe we can start snake_casing them

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:31):

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

view this post on Zulip Gabriel Ebner (Apr 25 2019 at 12:31):

ℭ𝔬𝔪𝔪ℜ𝔦𝔫𝔤

view this post on Zulip 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

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:34):

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

view this post on Zulip Keeley Hoek (Apr 25 2019 at 12:34):

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

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:34):

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

view this post on Zulip Keeley Hoek (Apr 25 2019 at 12:35):

hahaha now that is fancy

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:35):

Some option naming_convention in leanpkg.toml

view this post on Zulip Johan Commelin (Apr 25 2019 at 12:35):

Or namingConvention if you really want

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Apr 25 2019 at 12:37):

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

view this post on Zulip Keeley Hoek (Apr 25 2019 at 12:37):

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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Apr 25 2019 at 13:21):

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

view this post on Zulip Keeley Hoek (Apr 25 2019 at 13:23):

PascalCase camelCase

view this post on Zulip Johan Commelin (Apr 25 2019 at 13:24):

Oooh! So we should blame Blaise!

view this post on Zulip Edward Ayers (Apr 25 2019 at 13:58):

What does &@, mk_borrowed do?

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Apr 25 2019 at 16:13):

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

view this post on Zulip 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.

view this post on Zulip Simon Hudon (Apr 25 2019 at 16:21):

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

view this post on Zulip 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!

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip Sebastian Ullrich (Apr 26 2019 at 08:01):

No, not yet

view this post on Zulip 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?

view this post on Zulip Patrick Massot (Apr 26 2019 at 12:03):

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

view this post on Zulip Keeley Hoek (Apr 26 2019 at 12:15):

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

view this post on Zulip 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.

view this post on Zulip Kenny Lau (Apr 26 2019 at 15:21):

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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)

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip Mario Carneiro (Apr 26 2019 at 23:29):

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

view this post on Zulip Mario Carneiro (Apr 26 2019 at 23:29):

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

view this post on Zulip 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

view this post on Zulip Mario Carneiro (Apr 26 2019 at 23:31):

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

view this post on Zulip 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.

view this post on Zulip 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

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip 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 :-)

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Sebastian Ullrich (Apr 29 2019 at 11:05):

What Patrick said

view this post on Zulip 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.

view this post on Zulip Sebastian Ullrich (Aug 16 2019 at 10:27):

@Mario Carneiro

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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Patrick Massot (Aug 24 2019 at 10:36):

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

view this post on Zulip 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