How can I begin my LEAN4 and mathlib4. I have tried two ways

Stream: new members

[Liubo]

I am trying begin my LEAN4 with VSCode, and now I tried two ways.
first is in windows.
I prepared the enviroment like following:

---

elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

lean -version
Lean (version 4.7.0, x86_64-w64-windows-gnu, commit 6fce8f7d5cd1, Release)

---

then I used "lake new B001" created a new project and input following statement inside B001.lean.

---

-- This module serves as the root of the B001 library.
-- Import modules here that should be built as part of the library.
import «B001».Basic

#eval Lean.versionString

---

and I got correct message inside Infoview:

---

All Messages (1)
B001.lean:5:0
"4.7.0"

---

but when I try to add

---

require mathlib from git "https://github.com/leanprover-community/mathlib4"

---

into lakefile.lean
following message was output in Infoview:

---

c:\Users\xhsdo\.elan\toolchains\leanprover--lean4---stable\bin\lake.exe setup-file E:/users/sky/LEAN/p2/B003/B003.lean Init B003.Basic --no-build failed:

stderr:
error: missing manifest; use lake update to generate one
Invalid Lake configuration. Please restart the server after fixing the Lake configuration file.

---

then I tried to run:

---

lake update

---

mathlib: cloning https://github.com/leanprover-community/mathlib4 to '.\.lake\packages\mathlib'
error: .\.lake\packages\mathlib\lakefile.lean:10:7: error: unexpected token; expected identifier
error: .\.lake\packages\mathlib\lakefile.lean:11:7: error: unexpected token; expected identifier
error: .\.lake\packages\mathlib\lakefile.lean:12:7: error: unexpected token; expected identifier
error: .\.lake\packages\mathlib\lakefile.lean:13:7: error: unexpected token; expected identifier
error: .\.lake\packages\mathlib\lakefile.lean:14:7: error: unexpected token; expected identifier
error: .\.lake\packages\mathlib\lakefile.lean:15:7: error: unexpected token; expected identifier
error: .\.lake\packages\mathlib\lakefile.lean:139:2: error: unknown attribute [test_driver]
error: .\.lake\packages\mathlib\lakefile.lean: package configuration has errors

---

and inside ".\.lake\packages\mathlib\lakefile.lean":

---

require "leanprover-community" / "batteries" @ git "main"
require "leanprover-community" / "Qq" @ git "master"
require "leanprover-community" / "aesop" @ git "master"
require "leanprover-community" / "proofwidgets" @ git "v0.0.42"
require "leanprover-community" / "importGraph" @ git "main"
require "leanprover-community" / "LeanSearchClient" @ git "main"

---

"leanprover-community" was marked with red underline.
so what can I do now?

and the second way is in ubuntu 24.04.
VSCode was installed and .

---

elan --version
elan 3.1.1 (71ddc6633 2024-02-22)

lake --version
Lake version 5.0.0-6fce8f7 (Lean version 4.7.0)

lean -version
Lean (version 4.7.0, x86_64-w64-windows-gnu, commit 6fce8f7d5cd1, Release)

---

Then I used "lake new B001" created a new project and input following statement inside B001.lean.
But I got nothing inside Infoview.

so what can I do to continue? thanks very much.

[Daniel Weber]

Have you seen https://github.com/leanprover-community/mathlib4/wiki/Using-mathlib4-as-a-dependency ? You should also make sure that the content of your lean-toolchain file matches Mathlib's (which currently has leanprover/lean4:v4.12.0 there)

[Liubo]

tried and succeed, and now I can try following steps, thank you very much.