Topic: Problems Mac Instalation
Regivan Hugo Nunes Santiago (Nov 19 2020 at 19:29):
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:
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:
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.
Bryan Gin-ge Chen (Nov 19 2020 at 19:31):
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 (Nov 19 2020 at 20:08):
Dear Bryan, thank you very much. You have solved my problem.
Bryan Gin-ge Chen (Nov 19 2020 at 20:14):
Great, glad you got things working! Feel free to ask here if you have any other issues.
Last updated: May 08 2021 at 10:12 UTC