Is there a tutorial for lean's module and package system?

Stream: lean4

[Erika Su]

Currently, the documentaion only covers namespace and section.
I tried to understand lean's package and module system via lake's documentation and source code of some existent projects. Only to find confusion after numerous experiments.....

[Shreyas Srinivas]

There is no tutorial I can find. I have so far tried to follow the README file on lake's repo (https://github.com/leanprover/lake), and mathlib4's lakefile.lean

[Shreyas Srinivas]

the examples in the examples folder in the lake repository might also be useful guides

[Shreyas Srinivas]

A full tutorial would be really nice