Problems Mac Instalation

Stream: general

[Regivan Hugo Nunes Santiago]

Hi! I am trying to install Lean 3 in Mac OS. I have followed the "Getting Started" homepage and introduced the command:

/bin/bash -c "$(curl -fsSL https://raw.githubusercontent.com/leanprover-community/mathlib-tools/master/scripts/install_macos.sh)" && source ~/.profile

in order to install Lean and Mathlib. However, the following code in Visualcode:

import data.nat.basic
open nat

constant prime : ℕ → Prop
constant even : ℕ → Prop
constant odd : ℕ → Prop

#check ∀ x, (even x ∨ odd x) ∧ ¬ (even x ∧ odd x)
#check ∀ x, even x ↔ 2 ∣ x
#check ∀ x, even x → even (x^2)
#check ∀ x, even x ↔ odd (x + 1)
#check ∀ x, prime x ∧ x > 2 → odd x
#check ∀ x y z, x ∣ y → y ∣ z → x ∣ z

returns the following error:

-file 'data/nat/basic' not found in the search path
Use 'lean --path' to see where lean is looking, or https://leanprover-community.github.io/file-not-found.html for more

• invalid import: data.nat.basic
  could not resolve import: data.nat.basic

When I type: lean --path, I get:

{
"is_user_leanpkg_path": true,
"leanpkg_path_file": "/Users/lean02/.lean/leanpkg.path",
"path": [
"/Users/lean02/.elan/toolchains/stable/bin/../library",
"/Users/lean02/.elan/toolchains/stable/bin/../lib/lean/library"
]
}

However, the path: /Users/lean02/.lean/leanpkg.path, does not exists.

Can anyone help me? I think that if a change the path variable to point to mathlib I can solve this problem, however I do not know where is mathlib and where to put the right path to point to it.

Thank you in advance.

Regivan

[Bryan Gin-ge Chen]

Did you read the projects page which is linked at the bottom of the macOS install page? You shouldn't need to play around with paths; the leanproject utility should be handling all of this for you.

[Regivan Hugo Nunes Santiago]

Dear Bryan, thank you very much. You have solved my problem.

[Bryan Gin-ge Chen]

Great, glad you got things working! Feel free to ask here if you have any other issues.