Mathlib has moved to the new module system

Stream: mathlib4

[Kim Morrison]

Mathlib has just moved to Lean's new module system.

The module system allows for fast compilation, smaller olean file sizes, and better modular design. Take a look at this:

modulize.gif

Here I've modified a proof somewhere in the middle of Mathlib, saved the file, and then get an instant rebuild of Mathlib! The module system understands that proof irrelevance means downstream files don't need to be re-checked.

What do you need to know?

• If your work doesn't involve modifying import statements, you can get by not knowing anything new. :-)
• There's preliminary documentation at https://lean-lang.org/doc/reference/latest/The-Module-System/. Please read this first!
• By the time the module system matures from its current experimental status, there'll be further documentation.
• The lake exe shake tool will stop working (and will be temporarily disabled in CI), but there is a more powerful and sound replacement on the way.

Initially in Mathlib the main effect you'll see is fast recompilation if you only change proofs. But the module system will later allow us to do much fancier things, along the lines of Lean understanding that while the real numbers might be defined in terms of Cauchy sequences, there is a proper API barrier here. Changing even definitions about Cauchy sequences will only necessitate recompilation up to the construction of the reals, but not of all downstream uses of the reals.

The module system splits .olean files into several components. For now the lake exe cache system just downloads everything, but in the future it will get smarter, and the module system will enable us to significantly shrink the size of oleans which need to be downloaded to get started.

[Wrenna Robson]

This looks cool. If you add a theorem to a file but don't actually use that elsewhere, will that require a re-compilation of everything downstream?

[Wrenna Robson]

Naturally if you change a statement I can see that there would be issues but in that case in theory everything should still work.

[Jovan Gerbscheid]

I presume so, because it will change the behaviour of e.g. try exact my_theorem

[Wrenna Robson]

The potential for proper API barriers sounds really cool. I will repeat an observation I have made before: the concept of "proof API" in the sense that Lean and Mathlib communities use it is I think fairly novel - like I think a proper research paper exploring it and comparing it against similar notions etc. would be viable and useful.

[Wrenna Robson]

In my PhD dissertation I had to describe the concept but it was hard to find anything to cite on the matter!

[Kim Morrison]

Yes, if you add a public theorem, (which is the default throughout Mathlib at the moment because every file starts with public section) then that will require recompilation of everything downstream.

[Kim Morrison]

However, if you add a non-public theorem in X, then it will only require recompilation of modules which use import all X. (or transitive chains of import alls, right?)

[František Silváši 🦉]

Don't want to spam announce, so I'll hijack this a bit. The docs link in the announcement (4.26.0) is broken :(. It's this link.

This one works instead (when I manually remove -rc1).

[Kim Morrison]

František Silváši 🦉 said:

Don't want to spam announce, so I'll hijack this a bit. The docs link in the announcement (4.26.0) is broken :(. It's this link.

Fixed, much appreciated!

[Chris Henson]

Wrenna Robson said:

The potential for proper API barriers sounds really cool. I will repeat an observation I have made before: the concept of "proof API" in the sense that Lean and Mathlib communities use it is I think fairly novel - like I think a proper research paper exploring it and comparing it against similar notions etc. would be viable and useful.

I've had the same exact thought. It interacts with both the the software engineering and technical aspects in interesting ways. Like you say, I think if there's a depth of comparison to other systems it would make for a compelling paper.

[Yaël Dillies]

It looks like the import diff bot is broken, eg it doesn't mention any import increase in #29449, even though there is one

[Michael Rothgang]

Thanks for reporting, good catch! Let me CC @Damiano Testa @Bryan Gin-ge Chen about the import diff bot. (I don't have time today to investigate, sadly.)

[Nailin Guan]

Maybe not an appropriate place, but can we have this kind of big shift in announce priorior to the change itself? Also is it possible to to have auto fix for these kind of updates for PR? As when facing PR "A" depending on both PR "B" and "C" having conflicts, this is almost impossible to update smoothly (there are even more annoying case).

[Sebastian Ullrich]

Kim Morrison said:

The module system splits .olean files into several components. For now the lake exe cache system just downloads everything, but in the future it will get smarter, and the module system will enable us to significantly shrink the size of oleans which need to be downloaded to get started.

In particular, one immediate effect of this split and reduction of build dependencies is that the RAM necessary for both building and opening Mathlib has fallen by 2.8GB or 48%, reaching a value lower than at the end of the port to Lean 4 or ever since.
image.png

https://radar.lean-lang.org/repos/mathlib4/graph?m=build//maxrss&n=18000

[Eric Wieser]

Is the ram usage unchanged for downstream users importing Mathlib like FLT which aren't opted into the module system?

[Sebastian Ullrich]

It is, until they opt in as well (which we don't want to recommend yet for this release cycle, let's evaluate it on Mathlib first)

[Emily Riehl]

Does this new module system have any affect on open PRs? My #31101 is currently broken and I'm wondering if it has something to do with this. First I had a merge conflict with master, which I think was just a missing module at the start of the Mathlib.lean file. I updated that then ran lake exe mk_all (the PR creates a new file) but now have this error message:

Run cd pr-branch
+ cd pr-branch
+ env LEAN_ABORT_ON_PANIC=1 ../master-branch/scripts/lake-build-wrapper.py .lake/build_summary_lint.json lake exe runLinter Mathlib
Build progress [starting at 19/22]
✖ [7568/7568] Building Mathlib (4.8s)
Some required targets logged failures:
- Mathlib
error: build failed
Running linter on specified module: Mathlib
uncaught exception: object file '/home/lean/actions-runner/_work/mathlib4/mathlib4/pr-branch/.lake/build/lib/lean/Mathlib.olean' of module Mathlib does not exist

[Bas Spitters]

This looks great @Kim Morrison How does it compare to the OCaml/rocq module system, or with the wide theoretical literature on modules (Harper-Stone, F-ing modules, ..., or even more recent work based on modal type theory)

[Henrik Böving]

It has basically no relation to what ML calls modules at all

[Eric Wieser]

@Emily Riehl , that's the wrong part of the error; that's just saying "the linter failed because the build higher up failed"

[Eric Wieser]

Unfortunately github defaults to showing the last error not the first

[Bas Spitters]

Thanks @Henrik Böving so is there something the module system takes inspiration from?

[Emily Riehl]

@Eric Wieser thanks for the fix. I take it I'm supposed to write module at the start of any new Lean file now? What else should (naive) users know?

[Yaël Dillies]

module + replace import with public import (for now)

[Yaël Dillies]

I note that the backticks in the following error are misplaced:

Error: error: Mathlib.lean:1:0: cannot import non`-module` Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs from `module`

It should instead be

Error: error: Mathlib.lean:1:0: cannot import non-`module` Mathlib.Probability.Combinatorics.BinomialRandomGraph.Defs from `module`

[Damiano Testa]

Yaël Dillies said:

It looks like the import diff bot is broken, eg it doesn't mention any import increase in #29449, even though there is one

The script that counts transitive dependencies probably looks for lines that start with import ... instead of public import .... I don't have time now for a proper fix, but a quick one would be to simply change the regex to allow public before import...

[Yaël Dillies]

I foresee that a lot of PRs adding a (single) new file will forget to add @[expose] public section, because it won't break anything within the PR. Could we have a linter against files that contain only private declarations?

[Yaël Dillies]

I tried reviewing a PR (#27414) adding a single new file by copying its content in live.lean-lang.org. Unfortunately, the module invokation at the top fails with

object file '/home/lean4web/build/deploy-2025-11-16T18-00-12+00-00/MathlibDemo/.lake/packages/mathlib/.lake/build/lib/lean/Mathlib/Algebra/Order/Group/Ideal.olean' of module Mathlib.Algebra.Order.Group.Ideal does not exist

What gives?

[Riccardo Brasca]

Yaël Dillies said:

I foresee that a lot of PRs adding a (single) new file will forget to add @[expose] public section, because it won't break anything within the PR. Could we have a linter against files that contain only private declarations?

I was asking exactly this... and if someone has 2 minutes... #31815

[Yaël Dillies]

Ahahah, my prediction was quick to realise :laughing:

[Yaël Dillies]

Do we have opinions on whether import statements should be sorted by private vs public first, then alphabetically, or just alphabetically? ie

import A
public import B
import C

vs

public import B
-- A space here? Don't know!
import A
import C

vs

import A
import C
-- A space here? Don't know!
public import B

[Yaël Dillies]

The former looks ragged, but has the advantage of being the easiest to edit when privatising or publicising an import, although I foresee that this might be an uncommon operation to perform

[Yaël Dillies]

Btw, looking at it on Zulip, it's clear that public should be highlighted as a keyword just like import is. Anyone to update the lexer? :slight_smile:

[Thomas Murrills]

Yaël Dillies said:

I foresee that a lot of PRs adding a (single) new file will forget to add @[expose] public section, because it won't break anything within the PR. Could we have a linter against files that contain only private declarations?

I took a quick look because I expected this to be easy, but I'm actually not sure how we're meant to access the public/private constants in the current environment (per scope) in meta code, or even how to see the Visibility of a given declaration. No visibility information seems to be stored in the kernel environment, VisibilityMap itself is private, and Loogle doesn't turn up anything promising for Visibility...is the right approach just to import all and deal with the internals directly? Maybe this is a question for @Sebastian Ullrich ? :eyes: :)

[Thomas Murrills]

Here's a first stab. Documentation suggests that everything does indeed wind up in asyncConstsMap even if added synchronously with addDecl.

From experimentation, it seems like Lean adds _private to the front of non-public declarations, and includes all declarations in both the public and private VisibilityMap fields accessed here. I don't really understand why, or if this may change in the future, but this code should be robust to a change if it does.

I'd definitely like to get some feedback, though. :grinning_face_with_smiling_eyes:

linter code

module

public import Mathlib.Init
public import Lean.Environment
import all Lean.Environment

/-!
# Private module linter

This linter lints against nonempty modules that have only private declarations.
-/

meta section

open Lean Elab Command Linter

/-- The `privateModule` linter lints against nonempty modules that have only private declarations,
and suggests adding `@[expose] public section` to the top. -/
register_option linter.privateModule : Bool := {
  defValue := true
  descr := "Enable the `privateModule` linter, which lints against nonempty modules that have only \
    private declarations."
}

def privateModule : Linter where
  run stx := do
    if stx.isOfKind ``Parser.Command.eoi then
      unless getLinterValue linter.privateModule (← getLinterOptions) do
        return
      if (← getEnv).header.isModule then
        -- Wait for everything (necessary?)
        let _ := (← getEnv).checked.get
        unless (← getEnv).asyncConstsMap.public.revList.any
            (!(`_private).isPrefixOf ·.constInfo.name) do
          if (← getEnv).asyncConstsMap.private.size ≠ 0 then
            let topOfFileRef := Syntax.atom (.synthetic ⟨0⟩ ⟨0⟩) ""
            logLint linter.privateModule topOfFileRef
              "Module only contains private declarations.\n\n\
              Consider adding `@[expose] public section` at the beginning of the module."

initialize addLinter privateModule

[Thomas Murrills]

(This is at #31820...we'll see if it catches any more missed @[expose] public sections :grinning_face_with_smiling_eyes:)

[Thomas Murrills]

It caught exactly one: #31822 :)

[Kim Morrison]

Nailin Guan said:

Maybe not an appropriate place, but can we have this kind of big shift in announce priorior to the change itself? Also is it possible to to have auto fix for these kind of updates for PR? As when facing PR "A" depending on both PR "B" and "C" having conflicts, this is almost impossible to update smoothly (there are even more annoying case).

Indeed, there could have been a useful preliminary public announcement. We've been discussing it at length both in private maintainers/reviewers channels for some time, and also discussing it in the public #**nightly-testing> channel for the last two months. There's a balance to get right here: if we have something equally as dramatic come up in future, I'll try to make sure the information about it is a bit more visible. But realistically, we don't want to spam most users about things still in the future, and for those who want visibility into what is coming up, I recommend subscribing to (parts of) the #nightly-testing channel, which is open to all.

[Yaël Dillies]

Kim, I understand, but here writing a script would have been nice. It personally took me 2-3h fixing the conflicts on my 50 open PRs, even though they were (almost) all quite trivial.

[Nailin Guan]

I took nearly 2 hours only fixing approximately 1/3 of my nearly 50 open PRs, although some difficulties caused by github. Cache broken make this really having some difficulties.

Also, I believe a short announce is always good (at least in my opinion). Also, if in some cases it is hard to have a script, is it possible to have a time with parallel system, leaving some time for the change? Maybe this idea isn't appropriate here as this is from migrating to fork.

[Nailin Guan]

Kim Morrison 說：

Nailin Guan said:

Maybe not an appropriate place, but can we have this kind of big shift in announce priorior to the change itself? Also is it possible to to have auto fix for these kind of updates for PR? As when facing PR "A" depending on both PR "B" and "C" having conflicts, this is almost impossible to update smoothly (there are even more annoying case).

Indeed, there could have been a useful preliminary public announcement. We've been discussing it at length both in private maintainers/reviewers channels for some time, and also discussing it in the public #**nightly-testing> channel for the last two months. There's a balance to get right here: if we have something equally as dramatic come up in future, I'll try to make sure the information about it is a bit more visible. But realistically, we don't want to spam most users about things still in the future, and for those who want visibility into what is coming up, I recommend subscribing to (parts of) the #nightly-testing channel, which is open to all.

Also, there are different priorior, I believe this thread should at least appear before the update PR, this is at least 2 hours later than the update, within these time we can only get random instructions from the ones online.

[Michael Rothgang]

My understanding is that having a time with and without the module system coexisting in mathlib would not have worked well. That said, a migration script would have been helpful.

[Sebastian Ullrich]

@Thomas Murrills I think you'll simply want to use env.constants.map₂ as before and filter by isPrivateName

[Kim Morrison]

@Yaël Dillies, @Nailin Guan, @Michael Rothgang, if you have ideas for a script, please suggest / implement it! My experience so far is that it's not super scriptable, but I'm happy to see proposals.

[Yaël Dillies]

Yaël Dillies said:

Do we have opinions on whether import statements should be sorted by private vs public first, then alphabetically, or just alphabetically?

I now have the opinion that public and private imports should be separated, with the public ones coming first, and sorted alphabetically within each, ie

module

public import A
public import C

import B
import D

[Yaël Dillies]

Indeed, the procedure to reduce imports is to first reduce the public imports, potentially adding more private imports doing so, then reduce the private imports. The public and private imports usually come from widely different strata of mathlib (the public ones being much earlier, which also shows mathlib could gain a lot from wholly embracing modules), so it basically never happens that you privatise an existing public import, except when you're trying to reduce imports (meaning that a PR diff should basically never contain some pure unprivatising)

[Yaël Dillies]

I did some experiment with my existing PR #24912, and I am very pleased. I deliberately did not use @[expose] because all files but one don't contain defs at all, and the one that does contains a def that could be considered an implementation detail.

[Joseph Myers]

A possible improvement to linting for files with only private declarations would be to check for any private lemmas / definitions that aren't used at all in the whole project. This is particularly relevant for the mathlib archive: a typical file there should probably have only one or two main results that are public, with everything else being private, and it's very easy while developing something for the archive to end up with lemmas that you used at an earlier stage of the development but ended up not being needed in the final version (and are presumptively not of more general use, because more general lemmas should have gone in mathlib proper in the first place). So switching the archive to the convention that only the final main results are public would potentially allow detecting private lemmas that are no longer used and so should be deleted. (The same can apply to private lemmas in mathlib, it's just that there aren't so many such lemmas.)

[Dexin Zhang]

Is private now a legacy API in non-module system or orthogonal with the module system (especially the public keyword)? Thanks!

[Aaron Liu]

Is shake broken? I tried running it and it seems to be recommend removing many of the imports in most of the files.

[Kim Morrison]

Yes, shake no longer works. A replacement is coming soon. In the meantime, relax. :-)

[Niels Voss]

My understanding is that for old files, the primary changes are adding module to the top, making all the imports into public import, and adding @[expose] public section. But for new files, can we skip the @[expose] public section and be more judicious about what to expose?

[Niels Voss]

I noticed that

module
public def a : Nat := 5
public theorem mythm : a = 5 := rfl

fails, but replacing the rfl with a by rfl causes it to succeed. Are theorems whose proofs are just rfl treated specially for some reason (perhaps dsimp)?

[Sebastian Ullrich]

Yes but that has been true regardless of module for a while, lean#8419. That rfl is not even accepted here is new, of course.

[Nailin Guan]

Does find_home also fail because of the change? I got some strange result.
图片.png

[Junyan Xu]

module
theorem x : Nat.log2 1 = 0 := rfl -- `by rfl` also fails

fails:

Not a definitional equality: the left-hand side
  Nat.log2 1
is not definitionally equal to the right-hand side
  0

but if you remove the module then it works. Why is this and what should I do about it? It's causing the failure of #30144.

[Jovan Gerbscheid]

If you want your function binaryRecₖ to be kernel reducible for anyone who imports it, then you need to explicitly expose the value of the definition. This is done with the @[expose] tag.

[Junyan Xu]

Noted, thanks! The file doesn't currently build though due to the log2 defeq failure.

[Jovan Gerbscheid]

Since Nat.log2 has not been tagged with @[expose], the kernel cannot unfold it. Instead you will need to rewrite with Nat.log2_def (or any other lemma).

[Jovan Gerbscheid]

Oh and you don't need to use the @[expose] tag if you are already inside an @[expose] section, which is currently basically all of mathlib.

[Junyan Xu]

Why does it work without the module? Is the module system working as intended here?

[Jovan Gerbscheid]

Yes, being able to hide definitions is one of the features of the module system. Not using module gives you the old behaviour where everything can be unfolded.

[Junyan Xu]

I'm afraid my binaryRecₖ won't compute if Nat.log2 don't compute. I guess I should submit a PR to Lean 4 repo to add the @[expose] tag to Nat.log2.

[Junyan Xu]

Sorry for the noob question but how do I test the effect of Lean changes on mathlib? If I edit the file C:\Users\xujys\.elan\toolchains\leanprover--lean4---v4.26.0-rc2\src\lean\Init\Data\Nat\Log2.lean (where "Go to Definition" jumps to) there's no effect even if I restart the file or the server. I guess I can modify the lean-toolchain file in mathlib but it takes a release, not a commit ID like lake-manifest.json.

[Junyan Xu]

I've now opened lean4#11401 but can't verify whether it makes #30144 build.

[Jovan Gerbscheid]

The way to test this is slightly involved. You have to make a PR to lean core, but instead of branching off of master, you have to branch off of nightly-with-mathlib, because that branch has a corresponding mathlib version. If you branched off of master already, you can fix this by doing a git rebase onto nightly-with-mathlib (and a push --force). Then the automation will create a corresponding mathlib branch that depends on the toolchain from your lean PR.

Though I think this change is small enough where testing it on Mathlib may not be necessary.

[Michael Rothgang]

I just encountered a case of unexpected rebuilding: adding a set_option linter.flexible false in to a lemma causes a rebuild. Is this to be expected? (That linter is a syntax linter, hence does not/should not affect the generated proofs.)

[Damiano Testa]

Linters can emit (error) messages, so maybe that is the reason for rebuilding? Linters cannot affect the environment, but can also rewrite files, so they can certainly affect more than proofs, if you really wanted to!

[Damiano Testa]

I would like it if there were a new "category" of commands that could be inserted anywhere and has a guarantee that rebuilding is not required, though.

[Michael Rothgang]

Indeed, a way to say "I'm a harmless linter, don't look at me for rebuilding" might be nice.

[Sebastian Ullrich]

@Michael Rothgang Do you have a reproducer?

[Etienne Marion]

I am not sure I understand what @[expose] is for. If I understand correctly, it puts the body of a def in the public scope. But if I write

def foo : Bar := baz

lemma foo_def : foo = baz := by rfl

then if I need the value of foo, I can use foo_def, so I don't need to access the body of foo directly. Note that in the lemma above I need to use by rfl (or Eq.refl _) instead of rfl. I don't know why because

theorem and opaque never expose their body

so rfl should be considered in the private scope and should therefore be able to unfold foo, and indeed Eq.refl _ works. Is @[expose] only meant to allow for := rfl proofs to work, because for some reason they don't work otherwise? I feel like I am missing something, can anyone enlighten me please?

[Aaron Liu]

if you do rfl instead of by rfl it marks the theorem as a rfl-lemma

[Aaron Liu]

and it's not a rfl-lemma in the public scope since the body isn't exposed

[Etienne Marion]

In what situation would you use rfl in the public scope?

[Aaron Liu]

if you're rewriting by a rfl-lemma then you can use dsimp, for example

[Aaron Liu]

so that's why we mark rfl-lemmas specially

[Etienne Marion]

But dsimp would be used in a proof, so in the private scope, not the public scope.

[Aaron Liu]

if it's used in another module importing the one you wrote

[Etienne Marion]

So @[expose] is only needed to be able to unfold the definition in another module without relying on a lemma like foo_def that could be used with rw or simp or simp_rw? But if := rfl tags the lemma as a rfl lemma, then when you use rfl in another module it calls the lemma, it does not unfold the definition directly? Or does it?

[Aaron Liu]

if it's a rfl-lemma then that means you should be able to replace any occurrence of the lemma with just rfl

[Aaron Liu]

so rfl has to work in the public scope too

[Etienne Marion]

But you never use a lemma in the public scope

[Aaron Liu]

what does that mean

[Aaron Liu]

if it's a public theorem then you can use it in the public scope

[Etienne Marion]

When you use a lemma, you are inside a proof, and proofs are in the private scope

[Etienne Marion]

I don't understand why := by rfl would work without @[expose] but := rfl wouldn't work as they are the same lemmas in the end. Why should the latter being a rfl lemma change anything?

[Aaron Liu]

if I have another module which imports your file

[Aaron Liu]

then it's important that your lemma is still a rfl-lemma in my new file

[Aaron Liu]

my new file only imports the public scope of your file

[Aaron Liu]

so if the definition is in the private scope of your file, I can't unfold it

[Aaron Liu]

so it's not a rfl-lemma, which is a problem

[Etienne Marion]

Yes but my lemma := by rfl is in the public scope of my file.

[Etienne Marion]

So you can use this to unfold.

[Aaron Liu]

it's not the lemma that's the problem

[Aaron Liu]

it's the fact that it's a rfl-lemma

[Aaron Liu]

rfl-lemma means it has to be true by definition

[Jovan Gerbscheid]

The fact that theorem doesn't expose its body does not mean that you get access to all private scopes while writing the proof. It just means that once the theorem is proved, you can't look into the proof.

[Aaron Liu]

and if I'm stopped from unfolding stuff then it's no longer true by definition

[Etienne Marion]

How does rfl unfold the definition? Does it use the rfl-lemma, or the body of the definition directly?

[Jovan Gerbscheid]

The story about rfl lemmas is a red herring, it is only relevant to dsimp

[Etienne Marion]

Jovan Gerbscheid said:

The fact that theorem doesn't expose its body does not mean that you get access to all private scopes while writing the proof. It just means that once the theorem is proved, you can't look into the proof.

Ok fair point, you don't want to access the inside of a theorem for instance. But I would guess that the body of a def is always accessible in the private scope if you are in the same file as where the def is.

[Etienne Marion]

Jovan Gerbscheid said:

The story about rfl lemmas is a red herring, it is only relevant to dsimp

Ok, so rfl does not use rfl lemmas, it unfolds directly, so @[expose] is needed on a def if we want rfl to be able to unfold it in later imports. Do I get that right?

[Aaron Liu]

maybe?

[Aaron Liu]

so when you write a theorem and you prove it with := rfl it gets tagged with an attribute @[defeq]

[Aaron Liu]

and that's supposed to signal to tactics like dsimp that this lemma is a definitional equality

[Aaron Liu]

but of course this only works well when the lemma is actually a definitional equality

[Aaron Liu]

and that has to be a defeq in the scope that it gets used in

[Aaron Liu]

so if it's a public theorem then the @[defeq] attribute will double check that it's a definitional equality in the public scope, since even though the proof is rfl that proof was elaborated in the private scope which is allowed to unfold more things

[Etienne Marion]

Well if I did get it right then it answers my main question. However I am then still unsure why := by rfl is accepted but not := rfl.

Aaron Liu said:

but of course this only works well when the lemma is actually a definitional equality

This does not seem obvious to me. If you just apply a lemma, why do you care whether it is defeq or not? But this is more of a question about how dsimp works I guess. I personally never use it.

[Aaron Liu]

Etienne Marion said:

This does not seem obvious to me. If you just apply a lemma, why do you care whether it is defeq or not?

well I have a code example

def foo := 17
def bar : Fin foo := (12 : Fin 17)
def baz (n : Nat) (k : Fin n) : Prop := True

theorem foo_def : foo = 17 := rfl

example : baz foo bar := by
  simp only [foo_def]
  -- the goal is now `baz 17 bar`
  -- if foo is not defeq to 17 then this no longer typechecks
  sorry

[Aaron Liu]

and indeed if you change the proof of foo_def to by rfl then you get "simp made no progress"

[Jovan Gerbscheid]

I believe the question @Etienne Marion asked was not related to dsimp or simp

[Aaron Liu]

yes I'm showing why we sometimes care whether a lemma is defeq

[Etienne Marion]

Actually my initial question was not because it was more about the purpose of @[expose], but then I asked why defeq lemmas were treated in a special way, which is related to dsimp

[Etienne Marion]

I see. So there are certain situations where a defeq rewrite cannot be replaced by a propositional rewrite, here because you rewrite something which is part of a type, so you need defeq to be sure it still typechecks I guess?

[Aaron Liu]

oh I realized I haven't actually answered your initial question ("what is the purpose of @[expose]")

[Etienne Marion]

Etienne Marion said:

Jovan Gerbscheid said:

The story about rfl lemmas is a red herring, it is only relevant to dsimp

Ok, so rfl does not use rfl lemmas, it unfolds directly, so @[expose] is needed on a def if we want rfl to be able to unfold it in later imports. Do I get that right?

This is the conclusion I got.

[Etienne Marion]

Well I certainly learnt a lot, thank you!

[Yaël Dillies]

There's certainly something confusing here: The fact that rfl tags the lemma with @[defeq] is an implementation detail that should not influence whether the proof goes through or not. IMO it would be much less surprising if the criterion for tagging with @[defeq] were to be "the proof is rfl AND the definitions that need unfolding for the equality to be defeq all expose their body".

[Yaël Dillies]

If you agree, I'll open an issue in the lean repo

[Sebastian Ullrich]

It is not an implementation detail though, it is part of your module's interface and changing it will break downstream code. So there needs to be some syntactic marker.

[Edward van de Meent]

Right, so let that be an actual use of the @[defeq] attribute, and not this weird technicality that := rfl and := by rfl are different?

[Edward van de Meent]

And let the attribute check that the lemma actually is rfl in the public scope

[Sebastian Ullrich]

I will leave that part to @Joachim Breitner :)

[Etienne Marion]

Is one of the long-term goal of the module system to have files which strictly contain only defs, and these files should be the only ones to be public imported, and all the theorems are in separate files which should be imported?

[Edward van de Meent]

i don't think that's a goal, that's a means if anything. the relevant goal should be (and probably is) enabling increased compiler/typechecker efficiency.

[Edward van de Meent]

(among other goals of course)

[Edward van de Meent]

for an answer which better than a guess, i seem to recall the FRO roadmap mentioning the module system, as well as (i believe) goals and motivations for it.

[Etienne Marion]

The word "goal" may not be the right one indeed, I am just wondering if this something we should tend to. I’ll have a look at the roadmap.

[Etienne Marion]

I don't find much on https://lean-lang.org/fro/roadmap/y3/.

[Joachim Breitner]

I agree it’s somewhat confusing that

theorem … := rfl

is special (unlike := (rfl) or := by refl or anything else) and equivalent to

@[defeq] theorem … := (rfl)

and that one can think that it’s in bad taste. The goal here was to be pragmatic and do the right thing in the common case.

With this syntactic peculiarity explained, is there still something not working as intended?

[Etienne Marion]

Joachim Breitner said:

With this syntactic peculiarity explained, is there still something not working as intended?

No it's fine by me, thanks!

[Sebastian Ullrich]

Michael Rothgang said:

I just encountered a case of unexpected rebuilding: adding a set_option linter.flexible false in to a lemma causes a rebuild. Is this to be expected? (That linter is a syntax linter, hence does not/should not affect the generated proofs.)

@Michael Rothgang I tried removing one of the linter lines and nothing else was rebuilt.

$ git diff
diff --git a/Mathlib/Analysis/Complex/Arg.lean b/Mathlib/Analysis/Complex/Arg.lean
index 29831c3642..153f98f103 100644
--- a/Mathlib/Analysis/Complex/Arg.lean
+++ b/Mathlib/Analysis/Complex/Arg.lean
@@ -31,7 +31,6 @@ variable {x y : ℂ}
 namespace Complex

 -- Non-terminal simp, used to be field_simp
-set_option linter.flexible false in
 -- see https://github.com/leanprover-community/mathlib4/issues/29041
 set_option linter.unusedSimpArgs false in
 theorem sameRay_iff : SameRay ℝ x y ↔ x = 0 ∨ y = 0 ∨ x.arg = y.arg := by
$ lake build -v
...
⚠ [7651/7687] Built Mathlib.Analysis.Complex.Arg (1.2s)
...
Build completed successfully (7687 jobs).

[Jireh Loreaux]

Is there any reason that shifting from public imports to imports (where possible) needs to happen from the ground up? I suspect not, but I would like confirmation about this.

[Jovan Gerbscheid]

I have done this in a leaf file, making it use a (non-public) import to import a theorem from another file. So no, I don't see a reason this needs to be done from the ground up.

[Sebastian Ullrich]

I don't see one either

[Alastair Irving]

Is there an issue with the deprecated module linter and the new module system? I'm not getting a warning if I public import a deprecated module but I do get the warning if I remove public.

[Kim Morrison]

Probably. :-)

[Kim Morrison]

PR: https://github.com/leanprover-community/mathlib4/pull/32422

[Michael Rothgang]

Sebastian Ullrich said:

Michael Rothgang Do you have a reproducer?

@Sebastian Ullrich As I just told you in person, my attempts at finding a minimal reproducer failed (in that lake indeed rebuild very little \o/). I believe my original reproducer was on #28962:

• checkout e.g. 9bd0a0c4c1a6d7202a934880ded7bf61aa52d9c6
• apply the next commit 6e64ea345f5b4d342280a9c1e0d66778b9a0d711,
• verify that lean actually rebuilds things.

[Sebastian Ullrich]

@Michael Rothgang Cannot reproduce.

$ git checkout 9bd0a0c4c1a6d7202a934880ded7bf61aa52d9c6
$ lake exe cache --repo=grunweg/mathlib4 get
$ git checkout 6e64ea345f5b4d342280a9c1e0d66778b9a0d711 Mathlib/Analysis/Fourier/
$ lake build | cat
✔ [7646/7668] Built Mathlib.Analysis.Fourier.FourierTransformDeriv (13s)
Build completed successfully (7668 jobs).

[Michael Rothgang]

I see. Let me check again later and see if I can reproduce it myself. Sorry that this is so hard.

[Michael Rothgang]

I might finally have realised that this is about: let me take #32724 as an example. Building locally, I indeed see Lean doing no work --- but the CI workflow run does a lot of work. Is that indicative of something mathlib CI should fix?

[Sebastian Ullrich]

Ah, that makes sense. I think there was some previous discussion and also the future lake cache would change this anyway, but for now I would suggest CI to instead/also fetch the cache for a push event's before commit. I assume that would enable reuse in most cases.

[Michael Rothgang]

Makes sense, thanks! @Bryan Gin-ge Chen do you know how difficult it would be to make this change?

[Bryan Gin-ge Chen]

If we just have to checkout the parent commit and then run lake exe cache get on that instead / in addition, it shouldn't be too hard: we can probably add a few lines here? Happy to review a PR, otherwise I'll take a look at it when I can.

[Bryan Gin-ge Chen]

I created #33044 for this.

[Sebastian Ullrich]

How often do you think it happens that people push multiple commits at once? There is also a field for the commit before the push in the event data as mentioned

[Sebastian Ullrich]

Then again that doesn't help either if people e.g. push multiple times in quick succession

[Jovan Gerbscheid]

I do often push mutiple commits in a single push, with the purpose of labelling the changes more clearly.

[Bryan Gin-ge Chen]

I've switched to using github.event.before when it exists (falling back to HEAD^ otherwise).

[Jireh Loreaux]

I often push multiple commits at once because I don't want to overload the build runners when I'm in intermediate stages of a project (and I don't rebase before pushing because we squash-merge PRs to Mathlib anyway).

[Yaël Dillies]

I have opened #32541 as a way to start a discussion about basic tactic files: should those be re-exported by all files since they are basic, or should they instead be explicitly imported by the few files that actually need them?