## 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?

(deleted)

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

#### Kevin Buzzard (Oct 21 2019 at 16:13):

Is that arrow defined to mean something in Lean now?

#### Patrick Massot (Oct 21 2019 at 16:13):

It used to be some relator thing

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

#### Patrick Massot (Oct 21 2019 at 16:14):

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

#### Patrick Massot (Oct 21 2019 at 16:14):

Especially the deletion of relator.lean.

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

(note this is now in mathlib)

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

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

#### Patrick Massot (Oct 21 2019 at 16:17):

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

#### Kevin Sullivan (Oct 21 2019 at 16:41):

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

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