How does Lean4 module/package system work?

Stream: general

[StructSeeker]

I have checked up Lean4 Manual and can't find any content explaining these contents. For example, does a folder/a file counts as a namespace or not, what need/can be imported or open, how to use/create packages...... It reminds of the horrible documentation of coq on its module.

[Henrik Böving]

The concept of namespaces and modules are entirely unrelated. You create declarations in a namespaces with the namespace NAME <decls> end syntax. In theory arbitrary files can "break into" arbitrary namespaces as they wish. A namespace can be open-ed. Modules are simply files so if we have DirA/DirB/FileA.lean you import DirA.DirB.FileA. You will want to use lake for your project management. That's about all there is to know.

[StructSeeker]

Henrik Böving
What about relative path import and visibility? I hope there will be specific documentation in manual......

[Henrik Böving]

There are no relative path imports. If you are referring to things like protected or private with visibility those do exist in Lean but due to the fact that the type theory necessarily has to be able to look through definitions they are a little loose. protected means "If you open the namespace of this decl this decl in particular won't be exposed. This is useful for decls that have very common names like say add. private means private as you might be used to from OOP style languages. However in theory the type theory is still capable to look through a private if you put enough effort into it.

[StructSeeker]

thanks! Hopefully these will be added to documentation...

[Marc Huisinga]

StructSeeker said:

thanks! Hopefully these will be added to documentation...

The end of chapter 2 and the entirety of chapter 6 in TPIL4 might be helpful for you: https://leanprover.github.io/theorem_proving_in_lean4/