MacOS Install Help

Stream: new members

[North Eastern Ohio Mac Developer]

Hi,

I'd like to make an attempt at learning the basics of LEAN. (My background is in MacOS app development in Objective-C, with about 10 years experience, but I've been away from coding on a daily basis for about 8 years and my math background is not very strong.) I attempted to start getting an environment set-up using the instructions at:

https://leanprover-community.github.io/install/macos_details.html

Specifically, I downloaded elan-x86_64-apple-darwin.tar.gz and ran the elan-init tool. It output:

info: syncing channel updates for 'stable'
info: latest update on stable, lean version v4.11.0
info: downloading component 'lean'

Total: 194.6 MiB Speed: 540.8 KiB/s
info: installing component 'lean'
info: default toolchain set to 'stable'

stable installed - Lean (version 4.11.0, x86_64-apple-darwin22.6.0, commit ec3042d94bd1, Release)
Elan is installed now. Great!

Being a Mac developer my code editor has always been Xcode, but given it was suggested to use VS Code I did the blasphemous thing the instructions said to do and installed VS Code, and added the Lean4 extension. When creating a test file and entering "#eval 1+1" its successfully shows a value of 2 in a tooltip when I hover over the line as indicated in the install instructions page linked above.

Assuming I now had a successfully set-up environment I copied a snippit of LEAN code into the test file. The first line was "import Mathlib.NumberTheory.LucasLehmer" and the import statement was unlined in red with the following error in the tooltip:

unknown module prefix 'Mathlib'

No directory 'Mathlib' or file 'Mathlib.olean' in the search path entries:

/Users/my_username/.elan/toolchains/stable/lib/leanLean 4

Looking into the specified directory I do not see a MathLib library, so that would presumably explain the issue. Is this a separate download? Should it have been installed by the elan-init? Can I just download the MathLib from the URL below and drop it into the specified directory, or does the precise version need to match / sync with the build of LEAN4 that is installed?

https://github.com/leanprover-community/mathlib4/

Thanks.

P.S. Is there really any hard requirement to use VS Code? What is the basis of that requirement? Isn't this all just being passed to Clang? I can do that natively in Xcode. If anyone can point me to the source for whatever the Lean tie-ins are with VS Code (this leanprover extension) I'd love to take a look at that and see if it would be reasonable to re-create for Xcode integration.

[Kevin Buzzard]

To use mathlib you need to create a new Lean project with mathlib as a dependency. See https://leanprover-community.github.io/install/project.html . And yes there's a hard requirement to use an editor which is Lean-aware, and VS Code is a good example (emacs and vim are the two other possibilities, although there is more support for vim than emacs here; VS Code is by far the most popular).

[North Eastern Ohio Mac Developer]

@Kevin Buzzard Thanks. I was able to clone the mathematics_in_lean.git repo mentioned on the link you provided. And I see it imports MathLib. I'll examine these files, and try working through some of the exercises.

If you or anyone else can point it out, I'm still interested in where the code lives for this leanprover extension / integration with VS Code. Hopefully I can study how that works, and re-create the functionality in Xcode so I can rid my machine of this foul Microsoft product as quickly as possible.

[North Eastern Ohio Mac Developer]

I'm also a bit confused where the mathematics_in_lean project is pulling MathLib from. There still doesn't appear to be any MathLib in the toolchains/stable sub-directories on my system, and yet VS Code doesn't complain about the "import MathLib" when it is in a file inside the mathematics_in_lean directory, but it does complain when the same file is outside the mathematics_in_lean directory. And I don't see any MathLib inside any location inside the mathematics_in_lean directory either (like a local search path instead of a system search path). Very odd behavior.

[Rida Hamadani]

VScode lean extension repo: https://github.com/leanprover/vscode-lean4
Like Kevin says, you do not need to use vscode, check out https://github.com/Julian/lean.nvim/ and https://github.com/leanprover-community/lean4-mode. But feel free to write an extension for your favorite editor, I'm sure many others will benefit from it!
Lean is being imported to #mil because it is required in the lakefile.lean file, if you have already ran lake exe get cache (or a similar command) it should be present at the path .lake/packages/mathlib.

[Marc Huisinga]

North Eastern Ohio Mac Developer said:

Kevin Buzzard Thanks. I was able to clone the mathematics_in_lean.git repo mentioned on the link you provided. And I see it imports MathLib. I'll examine these files, and try working through some of the exercises.

If you or anyone else can point it out, I'm still interested in where the code lives for this leanprover extension / integration with VS Code. Hopefully I can study how that works, and re-create the functionality in Xcode so I can rid my machine of this foul Microsoft product as quickly as possible.

If you're curious about what features are provided by the Lean 4 VS Code extension (together with the Lean language server), you can read the manual: https://github.com/leanprover/vscode-lean4/blob/master/vscode-lean4/manual/manual.md. The most important features that are basically essential for working with Lean are described in the first five subsections of "Interacting with Lean files".