Zulip Chat Archive

Stream: new members

Topic: Weird executable version issue

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

Kevin Buzzard (Oct 21 2019 at 15:53):

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

Kevin Buzzard (Oct 21 2019 at 15:53):

(deleted)

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

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.

Kevin Sullivan (Oct 21 2019 at 15:57):

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

Reid Barton (Oct 21 2019 at 15:57):

elan show is a good place to start

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)

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?

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"}

Kevin Sullivan (Oct 21 2019 at 16:00):

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

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$

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.

Kevin Buzzard (Oct 21 2019 at 16:06):

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

Patrick Massot (Oct 21 2019 at 16:07):

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

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