Should I build lean by hand?

Stream: new members

[Dominic Steinitz]

I noticed that using the instructions here https://leanprover-community.github.io/install/macos.html gives me an x86_64 version and I would like an arm64 version. I can see build instructions here https://docs.lean-lang.org/lean4/doc/make/index.html. But is this "courageous" of me? And why is the default version x86_64 anyway?

[Dominic Steinitz]

Dominic Steinitz said:

I noticed that using the instructions here https://leanprover-community.github.io/install/macos.html gives me an x86_64 version and I would like an arm64 version. I can see build instructions here https://docs.lean-lang.org/lean4/doc/make/index.html. But is this "courageous" of me? And why is the default version x86_64 anyway?

"Courageous" is English for crazy ;-)

[Dominic Steinitz]

Well I didn't get very far with

dom@Wandle lean4 % nix develop
nix develop
trace: warning: The Nix-based build is deprecated

[Sebastian Ullrich]

Uninstalling elan from Homebrew and reinstalling it from its website should be sufficient

[Sebastian Ullrich]

Do remove ~/.elan between these steps though

[Dominic Steinitz]

I should run ./elan-init?

[Tom]

You can also install elan from the VSCode extension, if you're using that. That may be an easy way to do it. Either use "Lean4: Setup: Install Elan" from "Cmd + P", or select "Version Management -> Setup: Install Elan" from the Lean menu (the "forall" symbol)

HTH

[Tom]

I'm also on ARM 64 and IIRC, that's how I got things installed.

[Julian Berman]

It's also quite suspicious sounding that you got an x86_64 version from doing what you did. Did you install it with an x64 Homebrew? Or an ARM one? Something seems likely to need fixing there if you didn't install it with an x64 Homebrew, but I don't have time to do so myself.

[Dominic Steinitz]

I used the the script given here https://leanprover-community.github.io/install/macos.html and I think it must have installed the x86_64 version. I installed the desired elan version (arm64) here https://github.com/leanprover/elan/releases/tag/v3.1.1 and now I am in business.

[Dominic Steinitz]

Julian Berman said:

It's also quite suspicious sounding that you got an x86_64 version from doing what you did. Did you install it with an x64 Homebrew? Or an ARM one? Something seems likely to need fixing there if you didn't install it with an x64 Homebrew, but I don't have time to do so myself.

Are you also using copilot? My colleague is using it and it seems useful (especially for beginners like us). I currently cannot get it to work so if you are using it that would give another data point.

[Dominic Steinitz]

Sebastian Ullrich said:

Do remove ~/.elan between these steps though

I didn't use home-brew as I was advised against it. But removing ~/.elan and installing the desired elan worked thanks very much.

[Dominic Steinitz]

Tom said:

I'm also on ARM 64 and IIRC, that's how I got things installed.

Are you also using copilot? My colleague is using it and it seems useful (especially for beginners like us). I currently cannot get it to work so if you are using it that would give another data point.

[Dominic Steinitz]

Julian Berman said:

It's also quite suspicious sounding that you got an x86_64 version from doing what you did. Did you install it with an x64 Homebrew? Or an ARM one? Something seems likely to need fixing there if you didn't install it with an x64 Homebrew, but I don't have time to do so myself.

I think it was that I was using emacs which reported uname -m as x86_64 even though a terminal reported uname -m as arm64. After a mare with emacs, I now have arm64 both inside and outside of emacs. I still can't get LeanCopilot to work though.

[Julian Berman]

I do not use copilot. I'm happy to try to install it to tell you whether it works, but I am pretty sure others here (including on macOS) have gotten it working.

[Julian Berman]

I also noticed / remembered that the script you mentioned from the community page doesn't use Homebrew to do the install at all now. I know that's a recent change (and one I don't really think was necessary, but I think it was done to homogenize how elan gets installed across OSes).

[Tom]

@Dominic Steinitz

I am using copilot - the GitHub one. I think you mentioned "LeanCopilot" in another thread and I wasn't aware of that exists.

In general, it's decent in terms of at least giving me an idea of syntax and sometimes possible suggestions on how to implement functions but I find that I have to edit things a lot because Lean needs you to be a quite precise and copilot doesn't really "understand" logic and types.

Overall, I'd say it has been a net positive for learning, esp for e.g.

1. Writing little experiments as I go through e.g. FPiL
2. At least making me aware certain constructs even exist so I can go and try to look them up

I think because of the lack of code in Lean4 though, the training dataset must be relatively small and the suggestions sometimes seem to show "lean 3" syntax