any documentation on how to set up a package and use it

Stream: new members

[Xiyu Zhai]

In https://lean-lang.org/lean4/doc/organization.html, I couldn't find the guide on how to create a package, import it in another project. Is there any place I can learn more systematically about Lean's package management?

[Xiyu Zhai]

I believe lack of documentation is one critical source of llm's inabilities to correctly answer questions about Lean4.

[Xiyu Zhai]

It seems that we have lakefile.toml which is very similar to Cargo.toml except that one has to use [[require]] instead of [[dependency]]?