Zulip Chat Archive

Stream: lean4

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


Erika Su (Dec 29 2022 at 09:57):

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 (Dec 30 2022 at 01:59):

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 (Dec 30 2022 at 02:02):

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

Shreyas Srinivas (Dec 30 2022 at 02:03):

A full tutorial would be really nice


Last updated: Dec 20 2023 at 11:08 UTC