Zulip Chat Archive

Stream: general

Topic: Lean 3.4.2


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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:07):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:07):

Just that

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

view this post on Zulip Patrick Massot (Jan 06 2019 at 21:08):

(deleted)

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:08):

use lean#1982

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:10):

I'm not sure lean#1983 is correct

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:10):

Yeah, that's at most fixing a symptom

view this post on Zulip Patrick Massot (Jan 06 2019 at 21:11):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:11):

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:12):

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:14):

the doc PR seems innocuous enough

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:14):

lean#1960

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:16):

can we get coinductive_predicates removed from lean core?

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:16):

that should really be in mathlib instead

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:18):

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:19):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:21):

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:21):

You want me to make a PR?

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:22):

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:22):

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:23):

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:24):

it might be in some tests

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:25):

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

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

view this post on Zulip Mario Carneiro (Jan 06 2019 at 21:25):

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

view this post on Zulip Simon Hudon (Jan 06 2019 at 21:32):

I second the suggestion :)

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:41):

done. I've removed the token as well.

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:41):

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

view this post on Zulip Simon Hudon (Jan 06 2019 at 21:42):

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

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:42):

Then you can introduce it there

view this post on Zulip Simon Hudon (Jan 06 2019 at 21:43):

I withdraw my objection then

view this post on Zulip Simon Hudon (Jan 06 2019 at 21:43):

Thanks!

view this post on Zulip Simon Hudon (Jan 06 2019 at 21:44):

What's up with the MacOS build?

view this post on Zulip Sebastian Ullrich (Jan 06 2019 at 21:47):

I don't know

view this post on Zulip Simon Hudon (Jan 06 2019 at 21:48):

Mystery!

view this post on Zulip Bryan Gin-ge Chen (Jan 09 2019 at 16:50):

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

view this post on Zulip Sebastian Ullrich (Jan 09 2019 at 17:05):

Something is broken

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 22:24):

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

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

view this post on Zulip Kevin Buzzard (Jan 09 2019 at 22:26):

The issue Mario had in live coding

view this post on Zulip Gabriel Ebner (Jan 10 2019 at 08:13):

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

view this post on Zulip Jeremy Avigad (Jan 10 2019 at 08:19):

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

view this post on Zulip Rob Lewis (Jan 10 2019 at 08:20):

You could also use mine.

view this post on Zulip Gabriel Ebner (Jan 10 2019 at 08:23):

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

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

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

view this post on Zulip Johan Commelin (Jan 11 2019 at 11:46):

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

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

view this post on Zulip Johan Commelin (Jan 11 2019 at 11:48):

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

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

view this post on Zulip Kenny Lau (Jan 11 2019 at 12:26):

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

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

view this post on Zulip Johan Commelin (Jan 11 2019 at 12:26):

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

view this post on Zulip Chris Hughes (Jan 11 2019 at 12:26):

mathematicians care about lists.

view this post on Zulip Kenny Lau (Jan 11 2019 at 12:27):

@Johan Commelin it looks very like a Lie bracket

view this post on Zulip Kevin Buzzard (Jan 11 2019 at 12:27):

Not enough to take something as important as [

view this post on Zulip Kevin Buzzard (Jan 11 2019 at 12:27):

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

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

view this post on Zulip Reid Barton (Jan 11 2019 at 14:16):

In Lean 4 it could be scoped somehow I guess

view this post on Zulip Sebastian Ullrich (Jan 11 2019 at 14:21):

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

view this post on Zulip Sebastian Ullrich (Jan 18 2019 at 15:07):

Lean 3.4.2 has been released

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

view this post on Zulip Sebastian Ullrich (Jan 18 2019 at 15:17):

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

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

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

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

view this post on Zulip Patrick Massot (Jan 18 2019 at 15:46):

But we now have two open PR switching to Lean 3.4.2

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

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

view this post on Zulip Kenny Lau (Jan 20 2019 at 20:59):

so why aren't we upgrading to 3.4.2?

view this post on Zulip Mario Carneiro (Jan 21 2019 at 01:30):

still some build issue in the PR

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

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

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

view this post on Zulip Bryan Gin-ge Chen (Jan 21 2019 at 02:35):

Green now! :tada:

view this post on Zulip Mario Carneiro (Jan 21 2019 at 03:51):

merged now

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

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

view this post on Zulip Johannes Hölzl (Jan 21 2019 at 10:14):

done

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

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

view this post on Zulip Kevin Buzzard (Jan 22 2019 at 17:01):

e.g. fa2e3991e1199afa8029c5417c2f719b3a326a77 I guess

view this post on Zulip Kevin Buzzard (Jan 22 2019 at 17:01):

(not that I checked...)

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

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

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

view this post on Zulip Patrick Massot (Jan 22 2019 at 17:30):

There is already a branch doing that

view this post on Zulip Patrick Massot (Jan 22 2019 at 17:30):

But I guess we could have a release tag as well

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

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

view this post on Zulip Edward Ayers (Jan 24 2019 at 11:42):

FIXED

view this post on Zulip Edward Ayers (Jan 24 2019 at 11:43):

my bad

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

view this post on Zulip Edward Ayers (Jan 24 2019 at 13:28):

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

view this post on Zulip Johan Commelin (Jan 24 2019 at 13:58):

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

view this post on Zulip Jean Lo (Jan 24 2019 at 14:39):

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.

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

view this post on Zulip Jean Lo (Jan 24 2019 at 15:29):

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?

view this post on Zulip Sebastian Ullrich (Jan 24 2019 at 15:31):

Are you sure you're calling the right lean?

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

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

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

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

view this post on Zulip Kevin Buzzard (Jan 24 2019 at 16:09):

@Reid Barton will though.

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

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

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

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

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

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

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

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

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

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

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

view this post on Zulip Kenny Lau (Jan 29 2019 at 20:57):

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

view this post on Zulip Kenny Lau (Jan 29 2019 at 20:58):

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

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

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

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

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

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

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