lake in lean4

Stream: new members

[Valera]

I read documentatoin, and see that lake is deprecated and merged into lean4 itself now. What is the advised method of initializing a new project, and can somebody share some link to a simple lean project, that imports something from mathlib, or a documentation on how imports should be handled today

[Patrick Massot]

Only the separate repository is deprecated. The tool itself is still lake.

[Valera]

Patrick Massot said:

Only the separate repository is deprecated. The tool itself is still lake.

So if I need a new project, that will use mathlib4, I do lake new my_project && touch my_project/leanpkg.toml, then put

[dependencies]
MathLib4 = {git = "https://github.com/leanprover-community/mathlib4", rev = "<fill_me_in>"}

in there?

And then in non-production environment, -say I just need to prove few simple theorems, I would make a new file for each like my_project/MyProject/theorem_{number}.lean, importing import mathlib4.xxx at their tops?

[Ruben Van de Velde]

I suggest you use lake new my_project math which adds the dependency automatically

[Patrick Massot]

Valera you are mixing two versions of Lean here. leanpkg.toml is a Lean 3 file. There is no such file in the Lean 4 world.