Darwin file , bin

Stream: general

[Xhulja Kolgjini]

I downloaded the Darwin file after I kept getting the error :
toolchain 'stable' does not have the binary /Users/xhuljakolgjini/.elan/toolchains/stable/bin/leanpkg
Command '['leanpkg', 'new', 'file']' returned non-zero exit status 1.

and then I analysed document. There is a file named /bin/ that is unreadable and I don't know which extension to install to read it. there was no suggestions from the VS.
Screenshot-2023-10-11-at-20.00.08.png

[Xhulja Kolgjini]

Screenshot-2023-10-11-at-19.58.16.png

[Xhulja Kolgjini]

Screenshot-2023-10-11-at-20.11.11.png
opened in data spell and look at this mess...why can't my computer read it?

[Alex J. Best]

What are you trying to do? The recommended way to install lean is by installing elan following https://github.com/leanprover/elan#installation

[Alex J. Best]

And the reason you cant read it is that it is a binary file not a text file. All executables are stored in this format, if you opened word.exe you would see something similar. Executables are built by compilers and not edited by humans by hand

[Xhulja Kolgjini]

I went thru all the steps of downloading elan the right way and it still gives me the binary issue

[Xhulja Kolgjini]

Screenshot-2023-10-11-at-20.17.13.png

[Xhulja Kolgjini]

Screenshot-2023-10-11-at-20.19.27.png

[Alex J. Best]

What does elan toolchains list and which lean output

[Xhulja Kolgjini]

Screenshot-2023-10-11-at-20.21.17.png

[Xhulja Kolgjini]

(base) xhuljakolgjini@Xhuljas-MBP ~ % which lean
/usr/local/bin/lean

[Sebastian Ullrich]

What are you trying to do? leanpkg is a Lean 3 tool

[Xhulja Kolgjini]

so what should I install instead

[Xhulja Kolgjini]

I use M1 Pro chip

[Xhulja Kolgjini]

https://github.com/leanprover/lake/blob/master/README.md

[Alistair Tucker]

It looks like you already have a working Lean 4 installation. Are you working with an old project that uses Lean 3? If not, stick with Lean 4 because, for one thing, installing Lean 3 is a bit tricky on a new Mac.

[Alistair Tucker]

Yes lake is the new (for Lean 4) version of leanpkg.

[Xhulja Kolgjini]

lol I just tried

mkdir test
cd test
lake new test

[Xhulja Kolgjini]

and it worked

[Xhulja Kolgjini]

how do I uninstall leanpkg now

[Alistair Tucker]

Maybe elan toolchain uninstall leanprover-community/lean:3.49.1?

[Xhulja Kolgjini]

info: uninstalling toolchain 'leanprover-community/lean:3.49.1'
info: toolchain 'leanprover-community/lean:3.49.1' uninstalled

[Xhulja Kolgjini]

(base) xhuljakolgjini@Xhuljas-MBP ~ % elan toolchain list
stable (default)
leanprover/lean4:nightly-2023-02-04
leanprover/lean4:nightly-2023-08-23
leanprover/lean4:stable
leanprover/lean4:v4.2.0-rc1