Zulip Chat Archive

Stream: new members

Topic: Weird executable version issue


view this post on Zulip Kevin Sullivan (Oct 21 2019 at 15:51):

When I run lean --version from a terminal window within VS Code with a full path to the executable, I get one version.

$ /Users/sullivan/.elan/bin/lean --version
Lean (version 3.4.2, nightly-2018-08-23, commit b13ac127fd83, Release)

When I run lean --version from an OSX terminal window with the same full path to the executable, I get a different version.

$ /Users/sullivan/.elan/bin/lean --version
Lean (version 3.4.2, commit cbd2b6686ddb, Release)

What is going on here?

The version difference matters to me because it appears that the newest release version (86ddb) breaks the possibility to overload =>, an issue we're still investigating. Be that as it may, something strange and unexpected is happening. Or I'm crazy or just missing the obvious. Probably the latter. Can anyone enlighten me? I did by the way just erase .elan and download and install it again using option 1) proceed to install (default).

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 15:53):

Is the lean you're running an executable or a link?

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 15:53):

(deleted)

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 15:56):

Thanks, Kevin. It's the executable downloaded by the elan installer.

$ ls -l /Users/sullivan/.elan/bin/lean
-rwxr-xr-x 4 sullivan staff 5379104 Oct 21 09:26 /Users/sullivan/.elan/bin/lean

view this post on Zulip Reid Barton (Oct 21 2019 at 15:57):

Under elan, lean will check your leanpkg.toml file and invoke the lean binary of the toolchain corresponding to the specified version.

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 15:57):

Oh that's got to be it. Let me check.

view this post on Zulip Reid Barton (Oct 21 2019 at 15:57):

elan show is a good place to start

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 15:58):

elan show
installed toolchains


stable (default)
nightly-2018-08-23

active toolchain


stable (default)
Lean (version 3.4.2, commit cbd2b6686ddb, Release)

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 15:59):

So the issue is simply that lean is being run in a different directory on the two occasions?

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 15:59):

Yep.

[package]
name = "2102dev"
version = "0.1"
lean_version = "nightly-2018-08-23"
path = "src"

[dependencies]
mathlib = {git = "https://github.com/leanprover/mathlib", rev = "3ddfc239ddd757aa60cfa5a6f106bc68c5b8e1fc"}

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 16:00):

Thank you. It was of course "the obvious".

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 16:01):

I tried running lean in an old clone of mathlib and lo and behold, elan awoke!

$ cd mathlib-kbuzzard/
buzzard@brian:~/lean-projects/mathlib-kbuzzard$ lean --version
info: downloading component 'lean'
info: installing component 'lean'
Lean (version 3.4.1, commit 17fe3decaf8a, Release)
buzzard@brian:~/lean-projects/mathlib-kbuzzard$

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 16:03):

So the issue is simply that lean is being run in a different directory on the two occasions?

Yes, but this happens even when the same complete path to one executable is given. The "new" executable must be (doing the equivalent of) checking the toml file and redirecting execution to the old version (presumably at a different path somewhere in the 2018 nightly toolchain). This is what confused me.

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 16:06):

I know that all the "actual" binaries are in .elan/toolchains (at least for me)

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:07):

Yes, I think that .elan/bin/lean is only triaging to the correct version of lean.

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 16:09):

Ok. While I have you on the line ... all of the preceding was precipitated by an "unexpected token" error when processing a file that was working under the 2018 nightly version but that is no longer working under the stable 3.4.2 version. I checked the release notes, and there is no indication that anything should have changed. The problem occurs when I try to do this:

notation e1 ⇒ e2 := pImpl e1 e2

I now get "unexpected token" at the ⇒ symbol. Any ideas? That character by the way is \r= or \=>.

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 16:13):

Is that arrow defined to mean something in Lean now?

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:13):

It used to be some relator thing

view this post on Zulip Kevin Buzzard (Oct 21 2019 at 16:14):

so maybe when the relator change happened, the arrow was removed from the list of valid unicode tokens

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:14):

@Kevin Sullivan the commit you are looking for is https://github.com/leanprover/lean/commit/95fa4cfb0a8774570d67bb231c1ab088a94e12bb

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:14):

Especially the deletion of relator.lean.

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:15):

You now need to use https://github.com/leanprover-community/mathlib/blob/master/src/logic/relator.lean

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:16):

(note this is now in mathlib)

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:16):

All this understood provided I correctly recognized the arrow you were using.

view this post on Zulip Patrick Massot (Oct 21 2019 at 16:17):

Or maybe you want to use that symbol for something else than the relator thing?

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 16:41):

That must be it. Didn't see change in release notes. Maybe change in library.

view this post on Zulip Kevin Sullivan (Oct 21 2019 at 16:41):

#print ⇒

This also gives an unexpected token error at ⇒

Is #print not the right way to see the definition of a notation?


Last updated: May 11 2021 at 21:10 UTC