Lean 3.4.2

Stream: general

[Sebastian Ullrich]

I kind of forgot about it, and so did everyone else, I guess. Still, how about a Lean patch release in time for Lean Together? It looks like most discussions are back to complaining about general issues instead of specific bugs.

[Mario Carneiro]

is this adding anything new or is it just the fixes that are already on master?

[Sebastian Ullrich]

Just that

[Patrick Massot]

It looks like at least PR lean#1982 and lean#1983 wouldn't be hard to merge though

[Patrick Massot]

(deleted)

[Mario Carneiro]

use lean#1982

[Mario Carneiro]

I'm not sure lean#1983 is correct

[Sebastian Ullrich]

Yeah, that's at most fixing a symptom

[Patrick Massot]

Oh sorry, I read only the headline, and it seemed innocuous

[Sebastian Ullrich]

And 1982 is a triviality, I'm not opening that can of worms

[Mario Carneiro]

I guess this isn't an offer for actual maintenance of the core lib...

[Mario Carneiro]

the doc PR seems innocuous enough

[Mario Carneiro]

lean#1960

[Mario Carneiro]

can we get coinductive_predicates removed from lean core?

[Mario Carneiro]

that should really be in mathlib instead

[Sebastian Ullrich]

Right, @Simon Hudon mentioned that. I mean, I can wait.

[Mario Carneiro]

just saying, if you are prepping a release then now's a good time

[Sebastian Ullrich]

Yes, if someone wants to do it, I'll wait

[Mario Carneiro]

You want me to make a PR?

[Sebastian Ullrich]

Ah, it's even more trivial than I thought, yes?

[Mario Carneiro]

it should be just a clean remove, it's not used

[Mario Carneiro]

transfer is used, so that would be more work, but coinductive is not

[Mario Carneiro]

it might be in some tests

[Sebastian Ullrich]

I see coinductive is still registered as a built-in token, oops

[Mario Carneiro]

coinductive is a token in C++, but I think that was there even before the coinductive_predicates file

[Mario Carneiro]

it shouldn't be any harm to have it as an undefined token

[Simon Hudon]

I second the suggestion :)

[Sebastian Ullrich]

done. I've removed the token as well.

[Sebastian Ullrich]

Do I want to know what the hell is going on with the MacOS builds...?

[Simon Hudon]

I think we should keep the token though. We'll make use of it in mathlib

[Sebastian Ullrich]

Then you can introduce it there

[Simon Hudon]

I withdraw my objection then

[Simon Hudon]

Thanks!

[Simon Hudon]

What's up with the MacOS build?

[Sebastian Ullrich]

I don't know

[Simon Hudon]

Mystery!

[Bryan Gin-ge Chen]

Will a macOS binary be provided at some point or is something broken?

[Sebastian Ullrich]

Something is broken

[Kevin Buzzard]

Is it possible to stop mathlib recompiling a bunch of times on Windows?

[Kevin Buzzard]

Mathlib is horrible to compile and this issue is holding Chris and Kenny back. All the machines at Xena are Windows machines too.

[Kevin Buzzard]

The issue Mario had in live coding

[Gabriel Ebner]

Does anybody have a windows machine which can compile Lean to test out a hacky workaround?

[Jeremy Avigad]

You are welcome to use mine. But I'll be angry if you melt the keyboard.

[Rob Lewis]

You could also use mine.

[Gabriel Ebner]

Thanks, I'll get to you during coffee/lunch.

[Bryan Gin-ge Chen]

From comparing the macOS build logs here (failing) and here (working), it seems that the issue is that rvm added a new maintainer so that the old GPG key doesn't work anymore.

PR here: https://github.com/leanprover/lean/pull/1987

[Johan Commelin]

Can we turn the [ ... ] notation for list into a type class has_bracket?

[Johan Commelin]

Lie algebras have a binary operation denoted [x,y] and it is very common to write [n] for fin (n+1).

[Johan Commelin]

But maybe this wont actually solve the conflict with list notation... I dunno

[Sebastian Ullrich]

At some point, :: was overloaded to also mean vector.cons. Everybody who just wanted to use lists hated the ambiguity issues and so it was removed. I don't think overloading [...] (or making it a class) would fare any better.

[Kenny Lau]

@Johan Commelin I have changed the Lie bracket notation to use \([

[Johan Commelin]

So now there are 29 people who "just want to use lists" and 29 people who don't care about lists at all, and want to use [...] for other things. (Ooh, and there is 1 logician.)

[Johan Commelin]

@Kenny Lau I saw it. And it doesn't look anything like a Lie bracket.

[Chris Hughes]

mathematicians care about lists.

[Kenny Lau]

@Johan Commelin it looks very like a Lie bracket

[Kevin Buzzard]

Not enough to take something as important as [

[Kevin Buzzard]

and to render it unusable for all the things we use it for

[Reid Barton]

The [] list notation is used a lot in tactics in the core library, so it would be inconvenient to remove

[Reid Barton]

In Lean 4 it could be scoped somehow I guess

[Sebastian Ullrich]

Exactly, you can open just the notation you need in a file or even section

[Sebastian Ullrich]

Lean 3.4.2 has been released

[Bryan Gin-ge Chen]

I'm still waiting on the macos binary to appear and I happened to notice this broken build: https://travis-ci.org/leanprover/lean/jobs/481381766 does something need to be done for the smt2_interface ?

[Sebastian Ullrich]

Yes, I need to create lean-3.4.2 branches in those repos

[Kevin Buzzard]

Thanks so much for this Sebastian. As you have seen last week, there are more and more people working with Lean 3, both in mathematics and computer science, and even though we have clearly heard Leo's message that Lean 4 makes no guarantees of compatibility with Lean 3, I am sure that the growing user base and code base will ultimately teach you developers something about how Lean is used in the wild and in particular where it performs well and where it performs less well. You are an invaluable bridge between us and Leo at this time.

[Floris van Doorn]

How do I update lean using elan and set it to use 3.4.2 by default?

Floris@MSI MINGW64 /d/projects
$ elan update
info: syncing channel updates for 'stable'
info: latest update on stable, lean version v3.4.2
info: downloading component 'lean'
info: installing component 'lean'
info: checking for self-updates
info: downloading self-update

  stable updated - Lean (version 3.4.2, commit cbd2b6686ddb, Release)

Floris@MSI MINGW64 /d/projects/mathlib
$ elan which lean
C:\Users\Floris\.elan\toolchains\3.4.1\bin\lean.exe

Floris@MSI MINGW64 /d/projects/mathlib
$ elan default 3.4.2
info: downloading component 'lean'
info: installing component 'lean'
info: default toolchain set to '3.4.2'

  3.4.2 installed - Lean (version 3.4.2, commit cbd2b6686ddb, Release)

Floris@MSI MINGW64 /d/projects/mathlib
$ elan which lean
C:\Users\Floris\.elan\toolchains\3.4.1\bin\lean.exe

[Bryan Gin-ge Chen]

leanpkg.toml in mathlib is still specifying 3.4.1 so it will override the system default. The current master of mathlib also isn't compatible with 3.4.2 yet.

[Patrick Massot]

But we now have two open PR switching to Lean 3.4.2

[Johan Commelin]

If I understand elan correctly, the upgrade should be transparent, once mathlib has merged (one of) those PRs.

[Floris van Doorn]

Oh, that makes sense. So if the leanpkg.toml file states it uses version 3.4.2, then that version of Lean would also be automatically downloaded when running leanpkg build? That's neat!

[Kenny Lau]

so why aren't we upgrading to 3.4.2?

[Mario Carneiro]

still some build issue in the PR

[Mario Carneiro]

To all who are anxious to see this merged: Please make sure the PR actually builds before asking me to hurry up on merging it. I have other obligations with school right now, so I don't have a lot of time to devote to troubleshooting here

[Bryan Gin-ge Chen]

Sorry, I'd thought that the problem was a Travis cache issue. I'm taking a look at it now.

[Bryan Gin-ge Chen]

OK, I think the issue is that there's a constant foo in tests/finish1.lean and this conflicts with the coinductive foo in tests/coinductive.lean. I've renamed the latter foo to coind_foo and it works now. Pushing...

[Bryan Gin-ge Chen]

Green now! :tada:

[Mario Carneiro]

merged now

[Mario Carneiro]

the foo thing is a bit weird. @Gabriel Ebner You might know what's happening here - are all the tests executing in the same environment?

[Gabriel Ebner]

No, the tests are not run in the same environment. But we then we export all files into the plain-text format for leanchecker. This ensures that there are no clashes in the top-level declaration names, and that you can actually import all of mathlib together.
That said, now everything is in src/, we could easily exclude the tests here: just change that line to lean --recursive --export=mathlib.txt src/

[Johannes Hölzl]

done

[Patrick Massot]

Oh, that explains why we couldn't reproduce this failure locally. I'm not doing this leanchecker thing

[Kevin Buzzard]

@Mario Carneiro The 3.4.1 branch woes of mathlib should now be over, right? All you need to do is to point the branch at a random recent commit which worked with 3.4.1 and then never think about it again -- future mathlib commits are not guaranteed to work with 3.4.1 from now on.

[Kevin Buzzard]

e.g. fa2e3991e1199afa8029c5417c2f719b3a326a77 I guess

[Kevin Buzzard]

(not that I checked...)

[Bryan Gin-ge Chen]

The commit right before the 3.4.2 PR is this one https://github.com/leanprover/mathlib/commit/2c5bc214d1391659611591f4c6af222f2bea8e05

[Patrick Massot]

future mathlib commits are not guaranteed to work with 3.4.1 from now on.

For future reference, note that a stronger statement is true. mathlib is now guaranteed not to work with Lean 3.4.1. The reason is that some stuff moved from core library to mathlib. Hence trying to compile mathlib with Lean 3.4.1 will result in errors complaining some stuff is already defined.

[Simon Hudon]

Should we have a lean-3.4.1 tag for mathlib for those determined not to upgrade to Lean 3.4.2?

[Patrick Massot]

There is already a branch doing that

[Patrick Massot]

But I guess we could have a release tag as well

[Kevin Buzzard]

Aah! Is this logic.relator or something? I just had this because I download elan finally but still had 3.4.1 hard coded in VS code.

[Edward Ayers]

Hi I've just upgraded my system to Lean 3.4.2 and I'm confused about what I need to do to get mathlib working. I'm probably missing something obvs.
At the moment the logic/relator.lean file is broken in mathlib because it can't find left_unique. As far as I can tell the init/relator.lean has been removed from Lean 3.4.2
I've got the latest version of master for each.
Lean git commit: cbd2b6686 - (6 days ago) chore(*): release version 3.4.2
Mathlib git commit : 4aacae3 - (3 hours ago) feat(data/equiv/algebra): instances for transporting algebra across an equiv (#618)

[Edward Ayers]

FIXED

[Edward Ayers]

my bad

[Kevin Buzzard]

I had an analogous question but was too embarrassed to ask it here :-) The answer to my relator woes was "yes lean at the command line is 3.4.2 but you forgot that you told VS Code a direct link to lean 3.4.1"

[Edward Ayers]

example : "git fetch" ≠ "git pull" := dec_trivial

[Johan Commelin]

I think git pull = (git merge) ∘ (git fetch). It might even be defeq.

[Jean Lo]

how was this issue eventually resolved?

I'm experiencing a similar problem after getting 3.4.2 then attempting to compile mathlib (4aacae3). lean --version reports Lean (version 3.4.2, commit b13ac127fd83, Release), but attempting leanpkg buildin the mathlib directory results in many error noises, beginning with WARNING: Lean version mismatch: installed version is master, but package requires 3.4.2. Most of the errors that follow seem to be related to coinductive_predicates and relator.

[Bryan Gin-ge Chen]

The "officially-released" Lean 3.4.2 is at commit cbd2b6686ddb, so you may want to check that.

[Jean Lo]

oh, thanks.

I'm building lean following the instructions on this page: https://github.com/leanprover/lean/blob/master/doc/make/index.md

git log tells me in the cloned repo that my HEAD is on the correct commit, but after the build concludes lean -v still says b13ac127fd83. surely i'm missing something?

[Sebastian Ullrich]

Are you sure you're calling the right lean?

[Kevin Buzzard]

Just some comments in case they help: (1) the relator stuff was moved from core Lean to mathlib, so if you have complaints that it's being defined twice then this is evidence that you're using an old Lean and a new mathlib. (2) Any nightly binary of Lean released since 3.4.1 displays "version 3.4.2, ..." with lean -v and in particular just because it says 3.4.2 doesn't mean that it's a version of Lean released on or after the 3.4.2 release. If a major bug was found in Lean today and fixed by Leo tomorrow as a nightly then that nightly would I think say it was 3.4.3. Aah! In fact commit b13ac1... is from last August, so that's definitely your problem.

[Jean Lo]

yes, and attempting to fix that problem has led me to recompile lean from the correct-version source, but now I'm confused about why that hasn't changed the output of lean -v. how might i check whether i'm 'calling the right lean?'

[Bryan Gin-ge Chen]

try running which lean and seeing if the output matches the path to the lean that you built

[Kevin Buzzard]

Jean is using emacs so there is also the issue of which Lean emacs is using. I don't know how to figure that out.

[Kevin Buzzard]

@Reid Barton will though.

[Jean Lo]

@Bryan Gin-ge Chen oh lore, of course! I thought make would have tossed the binaries into /usr/bin for me D:

[Reid Barton]

I guess C-h v lean-rootdir and C-h v lean-executable-name will tell you what lean emacs is invoking

[Reid Barton]

I use elan which automatically picks the version of lean specified by the project, so I don't have to configure anything in emacs

[Jean Lo]

@Bryan Gin-ge Chen huh, I thought I could fix that by moving the contents of bin in the lean folder into /usr/bin by hand, but I don't know what lean-gdb.py and leanpkg.bat are and hesitate to try anything silly. What would be the correct way to proceed?

[Reid Barton]

I don't have a built Lean source tree on hand but if you want to install into /usr/bin then probably make install will do that

[Jean Lo]

I think that's done it. (except i'm a goof and now i have one copy of lean in /usr/bin and another in /usr/local/bin D: )

I'll go & see if everything works now. thanks so much for the help

[Bryan Gin-ge Chen]

Glad everything is working. I would recommend using elan in the long term, but it might be a pain to go and delete all the random copies of lean and fix paths etc. to get it working properly.

[Sebastian Ullrich]

while [ "$(which lean)" -ne ~/.elan/bin/lean ]; do sudo rm -f "$(which lean)"; done  # please don't sue me

[Kevin Buzzard]

I thought elan had all sorts of versions of Lean lying around, so it could use my 3.4.1 and 3.4.2 repos all at the same time?

[Sebastian Ullrich]

It does, but those are not in your PATH variable. elan actually refuses to install if you have an existing lean in your PATH to avoid this situation.

[Scott Morrison]

@Jean Lo, if tail end of this conversation didn't make sense: it's advised that you don't download, compile, and manage individual versions of Lean yourself anymore. Instead, you install elan and have it do all the work for you.

[Kenny Lau]

hmm... there are still occasional unnecessary recompiling on my windows surface pro vscode

[Kenny Lau]

it is faster to close and open vscode again...

[Joseph Corneli]

I'm also finding it quite slow under Emacs on Mac OS, and a bit flaky (e.g., it won't finish compiling a file). It seems faster and more stable on my Linux laptop, however.

[Kevin Buzzard]

I've seen no difference -- it used to work great, it still works great -- with VS Code and Ubuntu. I have seen some problems recently with random red areas appearing in VS Code corresponding to errors which have been fixed -- but I suspect this is a VS Code phenomenon rather than a Lean one.

[William DeMeo]

A few of my students tried the MacOS binary, all of them using VS Code. After installing the vscode lean extension and configuring the path, when they try to "Reload Lean server" they get errors. One got a segv and the other got

Lean: Unable to start the Lean server process: Error: spawn /Users/theusernameiput/lean-3.4.2-darwin/bin/lean ENOENT The lean.executablePath may be incorrect, make sure it is a valid Lean executable

Any hope to remedy this, or should I tell these students to try compiling from source?

(I suspect they would probably give up at that point and just rely on the browser version for the remainder of the semester. The browser version is impressively adequate for almost everything we'll do in this class, but still, it's less than ideal for homework assignments, since I want them to submit .lean files.)

[Bryan Gin-ge Chen]

Are they able to run lean from the command line?

Also, it's recommended now to use elan rather than to fool around with lean binaries by hand. Have you seen the videos that @Scott Morrison made here?

[Scott Morrison]

@William DeMeo, where did you find instructions to "configure the path"? This is not something they should be doing unless they're building from source, and not recommended.

[Kevin Buzzard]

I haven't compiled Lean from source for a very very long time. Elan is all you need