Sebastian Ullrich - The Lean module system

Stream: Lean Together 2026

[Markus Himmel]

Discussion thread for the talk.

[Snir Broshi]

What do backward.proofsInPublic and backward.privateInPublic do?
If I remove a usage of one of them in Mathlib, what would break and how would I attempt to fix it?

[Julian Berman]

Does the hiding of def bodies mean that what is considered "defeq abuse" and what isn't should reduce eventually a bit towards whether the def is @[expose] or not? And/or someone communicates to others whether the def is meant to be unfolded outside of its API by explicitly preventing doing so / not having it be exposed?

[Sebastian Ullrich]

I'll have to step away from Zulip for a bit but let me share my slides in the meantime!

Module System @ Lean Together-1.pdf

[Chris Henson]

I had two questions I didn't get a chance to ask:

• I have seen some PRs about the module system and reducibility, can you explain how they are related? (Thinking along the lines of Julian's defeq abuse question)
• For meta sections, is it now encouraged to isolate meta sections into their own files? I know the reference manual mentions a bit about this, but I don't quite understand the implications of files that were ported and currently have a mix of meta sections among other visibilities.

[Jireh Loreaux]

On the question of whether the module system will eventually be compulsory, Sebastian Ullrich indicated (paraphrasing): "probably not, but we want to get to a place where it always makes sense to use it."

I see a problem with this not eventually being compulsory. As use of the module system grows, it becomes increasingly important that its use is not just ubiquitous, but mandatory. Let's say I have a project X with several dependencies A, B, and C. The dependencies all use the module system, and, wanting to get its benefits, I adapt project X to the module system. Then later, I decide I would like to import a new project D. But, the author of D, out of not caring terribly much, or not wanting to bother, decided not to use the module system. Then I either can't import D into my project, or I am forced to downgrade away from the module system myself (and I can imagine cases in which project D is important enough to cause this downgrade to project X). Then you end up in a scenario in which the module system is not adopted widely solely because it's use is not mandatory, and a few important projects choose not to use it.

[Joachim Breitner]

Chris Henson schrieb:

I have seen some PRs about the module system and reducibility, can you explain how they are related?

If you have a def that is public but not exposed, then in downstream modules, it is opaque, so cannot be reduced (e.g. by rfl).

[Sebastian Ullrich]

Jireh Loreaux said:

I see a problem with this not eventually being compulsory.

Your reasoning makes sense. When we have made the module system always desirable, I do think we will want to at the very least heavily encourage its use (such as by making it the default, but don't nail me down on that thought quite yet) at which point it may not be much different from make it obligatory in case we don't want to go that far - at that point opting out of it would just become one of many ways you can ensure people will not want to use your library. But we will get to that decision in time and see what approach makes most sense for the ecosystem as a whole.

[Sebastian Ullrich]

Snir Broshi said:

What do backward.proofsInPublic and backward.privateInPublic do?
If I remove a usage of one of them in Mathlib, what would break and how would I attempt to fix it?

Please see §5.4 for a description and examples of these options. To eliminate privateInPublic, generally speaking you'll just have to think through whether you can restructure your file so that the private definition truly is used only in the private scope. To eliminate proofsInPublic uses that are still necessary even after resolving privateInPublic, it may be necessary to ensure the expected type of the by is fully known such as through additional type annotations.

[Sebastian Ullrich]

Chris Henson said:

• For meta sections, is it now encouraged to isolate meta sections into their own files? I know the reference manual mentions a bit about this, but I don't quite understand the implications of files that were ported and currently have a mix of meta sections among other visibilities.

I would say that's a good suggestion for bigger meta sections. If you remove the section and instead meta import that code, you also open up the code to use in non-meta contexts, but depending on the specific case that might not be too relevant.

[Riccardo Brasca]

I am hitting an error trying to use Modulize.lean:

lean --run ../lean4/script/Modulize.lean $(find FltRegular -name '*.lean') FltRegular.lean

../lean4/script/Modulize.lean:60:27: error(lean.synthInstanceFailed): failed to synthesize instance of type class
  OfNat text.Pos 0
numerals are polymorphic in Lean, but the numeral `0` cannot be used in a context where the expected type is
  text.Pos
due to the absence of the instance above

Am I doing something wrong?

[Sebastian Ullrich]

My bad, I noticed that breakage as well, now PRed at lean#12079

[Riccardo Brasca]

Thanks!

[Sebastian Ullrich]

You might need lean +nightly to run it but as it only looks at syntax, that shouldn't create any further issues

[Riccardo Brasca]

It almost works perfectly for me. The only issue is that for some reason it didn't add @[expose] public section to the this file. The file looks like any other file, but it contains only one declaration, without any open or namespace (and it only imports one single module from Mathlib, nothing else from the project). If you want I can try to minimize, but I will not have time today.

[Sebastian Ullrich]

Ah... because the script does only work syntactically, it doesn't know about lemma and thinks the file is empty. lean#12080 disabuses it of that idea.