The Module System
The module system is an experimental feature that allows for more fine-grained control over what information is exported from, and imported into, Lean files.
The main benefits of doing so are:
- Average build times
Changes to files that affect only non-exported information (e.g. proofs) will not trigger rebuilds outside of these files. Even when dependent files have to be rebuilt, those files that cannot be affected according to the
importannotations can be skipped.- API evolution
Library authors can trust that changes to non-exported information will not affect downstream users of their library.
- Avoiding accidental unfolding
Limiting the scope in which definitions can be unfolded allows for avoiding both reductions that should be replaced by application of more specific theorems as well as unproductive reductions that were not in fact necessary.
- Smaller executables
Separating compile-time and run-time code allows for more aggressive dead code elimination.
The module system is activated by prefixing a Lean file with the module keyword.
modules can only import other modules so adoption has to be done top-down.
Non-modules can import modules and will ignore all module-system-specific annotations.
At the time of writing, the module system is considered experimental and additionally guarded by the experimental.module option that has to be set to true in the project's Lake configuration file.
Of libraries shipped with Lean, only Init is currently fully ported.
The language semantics described below are close to final, but not all benefits described above are implemented yet.
