Zulip Chat Archive
Stream: new members
Topic: How to install Lean and mathlib?
Yono (Jul 28 2023 at 17:10):
I want to install mathlib with Ubuntu and vscode, but I heard using wsl, it is difficult. How do I do?
Notification Bot (Jul 28 2023 at 17:12):
A message was moved here from #general > PartialOrder and StarOrderedRing on IsROrC by Jireh Loreaux.
Scott Morrison (Jul 29 2023 at 03:43):
@Yono, the ubuntu installation instructions are at https://leanprover-community.github.io/install/debian.html.
Scott Morrison (Jul 29 2023 at 03:43):
Although I'm confused by your mention of WSL: do you actually want to install on Windows? If so, see https://leanprover-community.github.io/install/windows.html instead.
Yono (Jul 29 2023 at 05:44):
@Scott Morrison I have installed lean4, I want to do mathlib.
Scott Morrison (Jul 29 2023 at 05:46):
The links I have above include installing Mathlib
Yono (Jul 29 2023 at 05:47):
Does it not work in linux virtual environment?
Scott Morrison (Jul 29 2023 at 05:49):
As far as I'm aware it works just fine.
Yono (Jul 29 2023 at 05:53):
But I typed "import category_theory.category.Pointed" in test.lean, error "unknown package 'category_theory'" occured.
Scott Morrison (Jul 29 2023 at 05:54):
That looks like a mixture of Lean 3 and lean 4 naming. Where did you get it from?
Scott Morrison (Jul 29 2023 at 05:54):
import Mathlib.CategoryTheory.Category.Pointed has a chance.
Scott Morrison (Jul 29 2023 at 05:55):
(not at a computer, so untested)
Yono (Jul 29 2023 at 05:55):
Scott Morrison (Jul 29 2023 at 05:55):
That is Lean 3 code!
Yono (Jul 29 2023 at 05:55):
wow
Yono (Jul 29 2023 at 05:57):
where is mathlib for lean4 ? I searched the word "mathlib"
Scott Morrison (Jul 29 2023 at 05:57):
You need to be looking at the Mathlib4 repository.
Mario Carneiro (Jul 29 2023 at 05:57):
https://github.com/leanprover-community/mathlib4/
Yono (Jul 29 2023 at 05:59):
https://github.com/leanprover-community/mathlib4/blob/master/test/CategoryTheory/Coherence.lean, i typed the first line "import ..,", the result is same
Newell Jensen (Jul 29 2023 at 06:01):
You need to create a lean 4 project with lake and you need to have mathlib4 as a dependency https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency
Yono (Jul 29 2023 at 07:06):
I see. in lakefile.lean, Can I use import mathlib tactics? Can I rename lakefile.lean to other filename?
Yono (Jul 29 2023 at 07:12):
I typed lake +leanprover/lean4:nightly-2023-02-04 new test math, but I cannot impor Mathlib in test.lean in test-lean folder. (I typed lake exe cache get)
Yono (Jul 29 2023 at 07:22):
oh, i got it! thank you everyone!
Yono (Jul 29 2023 at 07:39):
mathlib (lean3) is too many, but mathlib (lean4) is only category theory? https://github.com/leanprover-community/mathlib4/tree/master/test/CategoryTheory
Patrick Massot (Jul 29 2023 at 07:42):
No, mathlib for Lean 4 has strictly more content than the Lean 3 version.
Riccardo Brasca (Jul 29 2023 at 07:42):
You can forget about Lean3. Mathlib has been fully ported to lean4. You can have a look ad the doc.
Patrick Massot (Jul 29 2023 at 07:42):
Yono, you are looking at the wrong folder, you want https://github.com/leanprover-community/mathlib4/tree/master/Mathlib.
Yono (Jul 29 2023 at 07:46):
thx! I completely misunderstood it.
Last updated: Dec 20 2023 at 11:08 UTC