## Stream: general

### Topic: Lean 3.4.2

#### Sebastian Ullrich (Jan 06 2019 at 21:05):

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 (Jan 06 2019 at 21:07):

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

Just that

#### Patrick Massot (Jan 06 2019 at 21:07):

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

(deleted)

use lean#1982

#### Mario Carneiro (Jan 06 2019 at 21:10):

I'm not sure lean#1983 is correct

#### Sebastian Ullrich (Jan 06 2019 at 21:10):

Yeah, that's at most fixing a symptom

#### Sebastian Ullrich (Jan 06 2019 at 21:11):

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

#### Mario Carneiro (Jan 06 2019 at 21:12):

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

#### Mario Carneiro (Jan 06 2019 at 21:14):

the doc PR seems innocuous enough

lean#1960

#### Mario Carneiro (Jan 06 2019 at 21:16):

can we get coinductive_predicates removed from lean core?

#### Mario Carneiro (Jan 06 2019 at 21:16):

that should really be in mathlib instead

#### Sebastian Ullrich (Jan 06 2019 at 21:18):

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

#### Mario Carneiro (Jan 06 2019 at 21:19):

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

#### Sebastian Ullrich (Jan 06 2019 at 21:21):

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

#### Mario Carneiro (Jan 06 2019 at 21:21):

You want me to make a PR?

#### Sebastian Ullrich (Jan 06 2019 at 21:22):

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

#### Mario Carneiro (Jan 06 2019 at 21:22):

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

#### Mario Carneiro (Jan 06 2019 at 21:23):

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

#### Mario Carneiro (Jan 06 2019 at 21:24):

it might be in some tests

#### Sebastian Ullrich (Jan 06 2019 at 21:25):

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

#### Mario Carneiro (Jan 06 2019 at 21:25):

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

#### Mario Carneiro (Jan 06 2019 at 21:25):

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

#### Simon Hudon (Jan 06 2019 at 21:32):

I second the suggestion :)

#### Sebastian Ullrich (Jan 06 2019 at 21:41):

done. I've removed the token as well.

#### Sebastian Ullrich (Jan 06 2019 at 21:41):

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

#### Simon Hudon (Jan 06 2019 at 21:42):

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

#### Sebastian Ullrich (Jan 06 2019 at 21:42):

Then you can introduce it there

#### Simon Hudon (Jan 06 2019 at 21:43):

I withdraw my objection then

Thanks!

#### Simon Hudon (Jan 06 2019 at 21:44):

What's up with the MacOS build?

I don't know

Mystery!

#### Bryan Gin-ge Chen (Jan 09 2019 at 16:50):

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

#### Sebastian Ullrich (Jan 09 2019 at 17:05):

Something is broken

#### Kevin Buzzard (Jan 09 2019 at 22:24):

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

#### Kevin Buzzard (Jan 09 2019 at 22:24):

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

The issue Mario had in live coding

#### Gabriel Ebner (Jan 10 2019 at 08:13):

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

#### Jeremy Avigad (Jan 10 2019 at 08:19):

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

#### Rob Lewis (Jan 10 2019 at 08:20):

You could also use mine.

#### Gabriel Ebner (Jan 10 2019 at 08:23):

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

#### Bryan Gin-ge Chen (Jan 10 2019 at 17:05):

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.

#### Johan Commelin (Jan 11 2019 at 11:46):

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

#### Johan Commelin (Jan 11 2019 at 11:47):

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

#### Johan Commelin (Jan 11 2019 at 11:48):

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

#### Sebastian Ullrich (Jan 11 2019 at 12:23):

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 (Jan 11 2019 at 12:26):

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

#### Johan Commelin (Jan 11 2019 at 12:26):

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 (Jan 11 2019 at 12:26):

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

#### Kenny Lau (Jan 11 2019 at 12:27):

@Johan Commelin it looks very like a Lie bracket

#### Kevin Buzzard (Jan 11 2019 at 12:27):

Not enough to take something as important as [

#### Kevin Buzzard (Jan 11 2019 at 12:27):

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

#### Reid Barton (Jan 11 2019 at 14:16):

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

#### Reid Barton (Jan 11 2019 at 14:16):

In Lean 4 it could be scoped somehow I guess

#### Sebastian Ullrich (Jan 11 2019 at 14:21):

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

#### Sebastian Ullrich (Jan 18 2019 at 15:07):

Lean 3.4.2 has been released

#### Bryan Gin-ge Chen (Jan 18 2019 at 15:13):

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 (Jan 18 2019 at 15:17):

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

#### Kevin Buzzard (Jan 18 2019 at 15:17):

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 (Jan 18 2019 at 15:44):

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 (Jan 18 2019 at 15:45):

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 (Jan 18 2019 at 15:46):

But we now have two open PR switching to Lean 3.4.2

#### Johan Commelin (Jan 18 2019 at 15:47):

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

#### Floris van Doorn (Jan 18 2019 at 15:49):

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 (Jan 20 2019 at 20:59):

so why aren't we upgrading to 3.4.2?

#### Mario Carneiro (Jan 21 2019 at 01:30):

still some build issue in the PR

#### Mario Carneiro (Jan 21 2019 at 01:37):

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 (Jan 21 2019 at 01:58):

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

#### Bryan Gin-ge Chen (Jan 21 2019 at 02:06):

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

merged now

#### Mario Carneiro (Jan 21 2019 at 03:51):

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 (Jan 21 2019 at 10:01):

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/

done

#### Patrick Massot (Jan 21 2019 at 11:30):

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

#### Kevin Buzzard (Jan 22 2019 at 17:00):

@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 (Jan 22 2019 at 17:01):

e.g. fa2e3991e1199afa8029c5417c2f719b3a326a77 I guess

#### Kevin Buzzard (Jan 22 2019 at 17:01):

(not that I checked...)

#### Bryan Gin-ge Chen (Jan 22 2019 at 17:11):

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

#### Patrick Massot (Jan 22 2019 at 17:22):

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 (Jan 22 2019 at 17:29):

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

#### Patrick Massot (Jan 22 2019 at 17:30):

There is already a branch doing that

#### Patrick Massot (Jan 22 2019 at 17:30):

But I guess we could have a release tag as well

#### Kevin Buzzard (Jan 22 2019 at 17:36):

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 (Jan 24 2019 at 11:39):

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

FIXED

#### Kevin Buzzard (Jan 24 2019 at 13:19):

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 (Jan 24 2019 at 13:28):

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


#### Johan Commelin (Jan 24 2019 at 13:58):

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

#### Jean Lo (Jan 24 2019 at 14:39):

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 (Jan 24 2019 at 14:48):

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

#### Jean Lo (Jan 24 2019 at 15:29):

oh, thanks.

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 (Jan 24 2019 at 15:31):

Are you sure you're calling the right lean?

#### Kevin Buzzard (Jan 24 2019 at 15:52):

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 (Jan 24 2019 at 16:06):

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 (Jan 24 2019 at 16:08):

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

#### Kevin Buzzard (Jan 24 2019 at 16:08):

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 (Jan 24 2019 at 16:09):

@Reid Barton will though.

#### Jean Lo (Jan 24 2019 at 16:12):

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

#### Reid Barton (Jan 24 2019 at 16:13):

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

#### Reid Barton (Jan 24 2019 at 16:15):

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 (Jan 24 2019 at 16:15):

@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 (Jan 24 2019 at 16:16):

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 (Jan 24 2019 at 16:20):

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 (Jan 24 2019 at 16:23):

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 (Jan 24 2019 at 16:25):

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


#### Kevin Buzzard (Jan 24 2019 at 16:27):

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 (Jan 24 2019 at 16:30):

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 (Jan 24 2019 at 21:20):

@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 (Jan 29 2019 at 20:57):

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

#### Kenny Lau (Jan 29 2019 at 20:58):

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

#### Joseph Corneli (Jan 30 2019 at 12:24):

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 (Jan 30 2019 at 12:39):

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 (Feb 13 2019 at 23:49):

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 (Feb 13 2019 at 23:59):

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 (Feb 14 2019 at 04:29):

@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 (Feb 14 2019 at 07:53):

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

Last updated: May 06 2021 at 21:09 UTC