releases of new Lean versions

Stream: general

[Alfredo Moreira-Rosa]

Is the new module behaviour documented somewhere ?

[Notification Bot]

A message was moved here from #announce > releases of new Lean versions by Sebastian Ullrich.

[Sebastian Ullrich]

Alfredo Moreira-Rosa said:

Is the new module behaviour documented somewhere ?

Yes, see https://lean-lang.org/doc/reference/latest/The-Module-System! This is a first documentation draft, now that the system is accessible to users, we will rapidly improve it. So do ask questions.

[Niels Voss]

I'm not actually sure how to enable the module system. I know we have to put experimental.module in the lakefile, but I am not actually super familiar with how to use lake so I don't really know what that means.

[Niels Voss]

Actually nevermind, I just found the lakefile for Std and basically we just add leanOptions = { experimental.module = true } to the lakefile below the "defaultTargets" line.

[Ruben Van de Velde]

And add module to the start of the file?

[Niels Voss]

I have two questions about the semantics of the module system:

• Suppose that B imports A and that B declares a private variable def foo : Nat := 5, for internal use exclusively. But then A later adds a public def foo : String := "bar". This seems to break B. Essentially, every time A declares a file in the root namespace, it has the potential to break backwards compatibility. I think the solution is to have A place everything in a namespace. Is this ideal?
• In my opinion, the structure of required imports is part of the public interface of a library. If foo is defined in MyLib.Alpha.Foo, then moving it to MyLib.Beta.Foo is a breaking change. And if MyLib.Alpha.Foo depends on MyLib.Gamma.Bar, which exposes a constant bar, a downstream library might import MyLib.Alpha.Foo and just assume that this means bar is now accessible as well. But then if MyLib removes the dependency of MyLib.Alpha.Foo on MyLib.Gamma.Bar, it could break the downstream library. Since imports must still be acyclic, I think this means that any large library will be constantly moving constants around between modules or at least changing the import graph as needed. Is there a way to allow these sorts of changes without potentially breaking downstream code?

[Sebastian Ullrich]

Niels Voss said:

I think the solution is to have A place everything in a namespace.

Yes, this has always been the case and your scenario appears to apply even before the module system.

Is there a way to allow these sorts of changes without potentially breaking downstream code?

No - removing a (public) import is a breaking change, this too has always been the case and should not be done without consideration. What is new is being able to demote an import to a private import, which likewise is a breaking change. I'm not sure I would agree that acyclicity of the import graph is a major driving factor in moving declarations in general. I think what we will see is that libraries will commit to one big breaking change when they reconsider what imports should stay public and after that the ability to use private imports will lead to a public import graph that is more stable than before, not less.

[Niels Voss]

Wait, let's say that the FLT project becomes sorry-free and there ends up being a single file called FLT.lean which has a single theorem for Fermat's Last Theorem. Also suppose mathlib has migrated to the module system. The private imports for that file would be enormous, but what would be the minimum possible public imports? Could you set up the file so that the public imports include hardly anything at all from Mathlib?

[Sebastian Ullrich]

You don't need any public Mathlib imports at all to state FLT. Well, one if you want to go Semiring.

[Niels Voss]

So in the most extreme case (not saying this is a good idea), mathlib could potentially be split into MathlibDefs and MathlibTheorems folders, where MathlibDefs contains every single public definition in mathlib and no public theorems, and doesn't publically import anything from MathlibTheorems, and no two files in MathlibTheorems publically import each other? And then the import graph of MathlibDefs would be very sparse, so we could for example have Mathlib.Data.Real.Basic have very few public imports (so it wouldn't need to publically import the rationals in any way)?

[Sebastian Ullrich]

I believe that separation already exists to a good degree specifically through the Basic files even before anyone was thinking about the module system? So instead of a complete reorganization, refining the existing splits, e.g. moving out even defs such as Real.equivCauchy that leak the implementation, should be sufficient here.

[Kim Morrison]

Except that in Mathlib the split is mostly via Defs files rather than Basic files (which is the convention in the lean4 repo).

[Kim Morrison]

We put quite a lot of effort into extending the "spine" of "Defs files only import other Defs files" as far as possible over the last year or two, and hopefully this will really start to provide some pay-offs with the module system.

If anyone would like to put effort into refactoring more definitions in mathlib onto this spine that would be appreciated and helpful!

[Kevin Buzzard]

Just wanted to flag one sad consequence of this approach, which is that whenever you want to see the basic API for definition X, jumping to definition and then reading the next 50 lines of code doesn't work :-( This was a strategy which was very effective before we made this defs/basic split.

[Niels Voss]

What exactly is the synergy between the spine of Defs approach and the module system? I can see how this would let Mathlib have a public api which is essentially just definitions, but I don't know if this actually makes development of mathlib easier because we still have to keep track of the private import chain so that we can avoid cycles, so it doesn't actually give any more flexibility in how mathlib's imports are structured.

[Niels Voss]

In more generality, suppose that in Mathlib we want to refactor A.lean to depend on B.lean, which has no public imports. But B.lean privately imports something which privately imports A.lean. Then this refactor will be invalid because it will create a cycle of private imports, even though there is no cycle of public imports. So in some sense, the fact that B.lean privately depends on A.lean is part of B.lean's public interface within Mathlib. (Once we get to a package outside of Mathlib, then B.lean's private dependency on A.lean is no longer part of B.lean's public interface, because it can't affect anything).

[Kenny Lau]

Kevin Buzzard said:

Just wanted to flag one sad consequence of this approach, which is that whenever you want to see the basic API for definition X, jumping to definition and then reading the next 50 lines of code doesn't work :-( This was a strategy which was very effective before we made this defs/basic split.

well now I suppose there's the approach of clicking the definition and then going to the file name in the explorer and changing it from Defs to Basic

[Kevin Buzzard]

And sometimes it's not in there! Because the definition was moved from a file other than Basic, because, well, it was a definition.

It's also not immediately obvious how to solve this with search, because at this point you don't know the names of the API lemmas. But of course you can muddle through in the end.

[Kenny Lau]

I do rely on Loogle a lot

[Kevin Buzzard]

Yes maybe that's the answer to this one.

[Chris Henson]

My standard workflow for discovering files is also to use loogle. I've had the thought previously that listing all the files by number of occurrences might be a nice feature. (I assume this is easy since each result already lists the file.)

[Sebastian Ullrich]

Niels Voss said:

What exactly is the synergy between the spine of Defs approach and the module system? I can see how this would let Mathlib have a public api which is essentially just definitions, but I don't know if this actually makes development of mathlib easier because we still have to keep track of the private import chain so that we can avoid cycles, so it doesn't actually give any more flexibility in how mathlib's imports are structured.

In general, minimizing the dependency closure of a module minimizes both the cases in which the module has to be rebuilt as well as the amount of data that has to be fetched and stored to work on the module.

[Niels Voss]

Ah I see, that makes sense. I was mainly thinking about the semantic advantages of modules, but I hadn't considered that there might be major performance benefits as well.

[Emily Riehl]

I have a more basic question that I've asked several times before but still don't understand the answer to (apologies to those who have tried to explain).

I'm running a Lean project using the Lean blueprint infrastructure.

1. How do I keep the local copy of mathlib relatively up to date?
2. If I want to immediately import the latest mathlib, how do I do this?

[Emily Riehl]

I've tried various things this morning that I can describe but they haven't yet succeeded in updating the files I want (the result of a PR that was merged overnight). What has happened is now lake build fails will a bunch of errors involving Batteries.something that I don't understand.

[Alfredo Moreira-Rosa]

image.png

[Emily Riehl]

This looks like you're in vscode. How do you make those menus appear?

[Etienne Marion]

Clicking on the forall symbol at the top

[Etienne Marion]

I also had these batteries errors recently when mathlib was updated to the last version of lean. The problem was that one of the dependencies had not been updated to the latest lean.

[Emily Riehl]

This seems to fail:

Cannot update dependency. Command output: info: toolchain not updated; already up-to-date info: mathlib: running post-update hooks ⚠ [3/19] Replayed Batteries.Data.String.Basic warning: Batteries/Data/String/Basic.lean:28:12: `String.Pos` has been deprecated: Use `String.Pos.Raw` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Pos` to `Pos.Raw x`). warning: Batteries/Data/String/Basic.lean:29:11: `String.atEnd` has been deprecated: Use `String.Pos.Raw.atEnd` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.atEnd` to `Pos.Raw.atEnd x`). warning: Batteries/Data/String/Basic.lean:30:13: `String.get` has been deprecated: Use `String.Pos.Raw.get` instead Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.get` to `Pos.Raw.get x`). warning: Batteries/Data/String/Basic.lean:31:29: `String.next` has been...

[Etienne Marion]

https://leanprover.zulipchat.com/#narrow/channel/113488-general/topic/Can't.20update.20BrownianMotion.20project/with/547109126

[Arthur Paulino]

I disagree that relying on Loogle is a good approach. "Go to definition" is too basic to depend on a project being hosted somewhere else. This is the kind of devex feature that's expected to work entirely on local files.

[Arthur Paulino]

Limited/broken GTD was my main heart break with Haskell. Lean's GTD as of v4.23 is amazing (as good as Rust's!). Please don't nerf it :tear:

[Kevin Buzzard]

I am a bit confused by what Arthur is talking about, but I also saw this weird batteries error recently.

When I bump a game I do this:
1) git checkout -b bump-mathlib
2) lake update or lake update mathlib (should both do the same as the VS Code point and click solution above)
3) lake exe cache get
4) lake build and expect only to see errors in my local files because of changes in mathlib which broke stuff. If I see errors in batteries then something has gone wrong and my gut feeling is that it's not my fault.
5) fix build, commit all changed files to the branch (which will be all the local lean files that broke, lake-manifest.json (if that didn't change then you didn't bump at all) and sometimes lean-toolchain (depending on whether the version of core lean that mathlib was using has changed since you last bumped; this changes once or twice a month) and then commit, push, check CI passes on github, and then merge.

[Arthur Paulino]

Kevin Buzzard said:

I am a bit confused by what Arthur is talking about

From your message above I understood that the "Go to definition" feature would no longer take you to the definition right away. That's what I'm talking about

[Kevin Buzzard]

@Emily Riehl I can confirm that I cloned your repo https://github.com/emilyriehl/infinity-cosmos, tried what I suggested, and got the same error as you.

[Kevin Buzzard]

...
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '8da40b72fece29b7d3fe3d768bac4c8910ce9bee'
info: mathlib: running post-update hooks
⚠ [7/20] Built Batteries.Data.String.Basic
warning: Batteries/Data/String/Basic.lean:28:12: `String.Pos` has been deprecated: Use `String.Pos.Raw` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Pos` to `Pos.Raw x`).
warning: Batteries/Data/String/Basic.lean:29:11: `String.atEnd` has been deprecated: Use `String.Pos.Raw.atEnd` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.atEnd` to `Pos.Raw.atEnd x`).
warning: Batteries/Data/String/Basic.lean:30:13: `String.get` has been deprecated: Use `String.Pos.Raw.get` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.get` to `Pos.Raw.get x`).
warning: Batteries/Data/String/Basic.lean:31:29: `String.next` has been deprecated: Use `String.Pos.Raw.next` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.next` to `Pos.Raw.next x`).
warning: Batteries/Data/String/Basic.lean:34:10: `String.next` has been deprecated: Use `String.Pos.Raw.next` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.next` to `Pos.Raw.next x`).
✖ [9/20] Building Batteries.Data.Array.Match
trace: .> LEAN_PATH=/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/batteries/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/Qq/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/aesop/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/proofwidgets/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/importGraph/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/LeanSearchClient/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/plausible/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/MD4Lean/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/BibtexQuery/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/UnicodeBasic/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/Cli/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/mathlib/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/checkdecls/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/doc-gen4/.lake/build/lib/lean:/media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/build/lib/lean /home/buzzard/.elan/toolchains/leanprover--lean4---v4.25.0-rc2/bin/lean /media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/batteries/Batteries/Data/Array/Match.lean -o /media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.olean -i /media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/batteries/.lake/build/lib/lean/Batteries/Data/Array/Match.ilean -c /media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.c --setup /media/buzzard/ExternalSSD1TB/lean-projects/infinity-cosmos/.lake/packages/batteries/.lake/build/ir/Batteries/Data/Array/Match.setup.json --json
...

[Kevin Buzzard]

I am not sure I understand this stuff any better than you do, but deleting .lake and trying lake exe cache get does not fix it. The error I get after doing that is the same. After lake update my lakefile.toml has

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.24.0"

and my lean-toolchain has leanprover/lean4:v4.25.0-rc2.

[Ruben Van de Velde]

That's odd. By the way, note that you have the rev key set for mathlib in your lakefile.toml, so lake update will not give you a more recent version

[Kevin Buzzard]

Somehow it's comments like this that exactly show the kind of problems which Emily and I face. I have no idea what this whole "rev" thing is, what the syntax of lakefile.toml is, I never touch this file myself, all that happens in practice with FLT is that people like Pietro occasionally make PRs called "bump mathlib" and I merge them, and then sometimes I type lake update and it works and then I bump mathlib myself. If you are suggesting that to make progress we are supposed to be editing system files which we don't understand then I would suggest that something is wrong with our set-up.

[Ruben Van de Velde]

What was the output of lake update?

[Kevin Buzzard]

This was the first thing I typed after cloning the repo and creating a bump branch. The output up until to the first error was

buzzard@brutus:~/lean-projects/infinity-cosmos$ lake update
info: doc-gen4: cloning https://github.com/leanprover/doc-gen4
info: doc-gen4: checking out revision '1cd7a1113090e216703e323e8fdcdf099f0a9c8a'
info: checkdecls: cloning https://github.com/PatrickMassot/checkdecls.git
info: mathlib: cloning https://github.com/leanprover-community/mathlib4.git
info: mathlib: checking out revision 'f897ebcf72cd16f89ab4577d0c826cd14afaafc7'
info: toolchain not updated; already up-to-date
info: Cli: cloning https://github.com/leanprover/lean4-cli
info: Cli: checking out revision '91c18fa62838ad0ab7384c03c9684d99d306e1da'
info: UnicodeBasic: cloning https://github.com/fgdorais/lean4-unicode-basic
info: UnicodeBasic: checking out revision 'e5aaa4949aad9a866aead1da5d5619e8decc8da7'
info: BibtexQuery: cloning https://github.com/dupuisf/BibtexQuery
info: BibtexQuery: checking out revision '1b05159ad44f220cec7489e65e6bc4b1e178b67f'
info: MD4Lean: cloning https://github.com/acmepjz/md4lean
info: MD4Lean: checking out revision '66aefec2852d3e229517694e642659f316576591'
info: plausible: cloning https://github.com/leanprover-community/plausible
info: plausible: checking out revision 'dfd06ebfe8d0e8fa7faba9cb5e5a2e74e7bd2805'
info: LeanSearchClient: cloning https://github.com/leanprover-community/LeanSearchClient
info: LeanSearchClient: checking out revision '99657ad92e23804e279f77ea6dbdeebaa1317b98'
info: importGraph: cloning https://github.com/leanprover-community/import-graph
info: importGraph: checking out revision 'd768126816be17600904726ca7976b185786e6b9'
info: proofwidgets: cloning https://github.com/leanprover-community/ProofWidgets4
info: proofwidgets: checking out revision '556caed0eadb7901e068131d1be208dd907d07a2'
info: aesop: cloning https://github.com/leanprover-community/aesop
info: aesop: checking out revision '725ac8cd67acd70a7beaf47c3725e23484c1ef50'
info: Qq: cloning https://github.com/leanprover-community/quote4
info: Qq: checking out revision 'dea6a3361fa36d5a13f87333dc506ada582e025c'
info: batteries: cloning https://github.com/leanprover-community/batteries
info: batteries: checking out revision '8da40b72fece29b7d3fe3d768bac4c8910ce9bee'
info: mathlib: running post-update hooks
⚠ [7/20] Built Batteries.Data.String.Basic
warning: Batteries/Data/String/Basic.lean:28:12: `String.Pos` has been deprecated: Use `String.Pos.Raw` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.Pos` to `Pos.Raw x`).
warning: Batteries/Data/String/Basic.lean:29:11: `String.atEnd` has been deprecated: Use `String.Pos.Raw.atEnd` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.atEnd` to `Pos.Raw.atEnd x`).
warning: Batteries/Data/String/Basic.lean:30:13: `String.get` has been deprecated: Use `String.Pos.Raw.get` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.get` to `Pos.Raw.get x`).
warning: Batteries/Data/String/Basic.lean:31:29: `String.next` has been deprecated: Use `String.Pos.Raw.next` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.next` to `Pos.Raw.next x`).
warning: Batteries/Data/String/Basic.lean:34:10: `String.next` has been deprecated: Use `String.Pos.Raw.next` instead

Note: The updated constant is in a different namespace. Dot notation may need to be changed (e.g., from `x.next` to `Pos.Raw.next x`).
✖ [9/20] Building Batteries.Data.Array.Match

[Ruben Van de Velde]

The lakefile is a list of dependencies for your project, and you can add some key-value pairs for each dependency

[Ruben Van de Velde]

One of them is rev, which you can use to make lake update stick to that particular revision of the dependency, rather than the most recent version

[Ruben Van de Velde]

I'll try to have a look when I'm not on mobile later

[Kevin Buzzard]

I mean in some sense I know everything you just said, but what I don't know is what the file is supposed to look like in order for me to never have to care about it ever again.

[Kevin Buzzard]

Or is "edit your lakefile.toml" actually supposed to be a part of the bump-mathlib workflow? (it wasn't part of the workflow I posted above, which I'm sure I've had some success with).

[Kevin Buzzard]

FLT right now says

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.25.0-rc1"

Is that wrong? Or right-but-I-am-doomed-to-failure-if-I-bump-rather-than-Pietro?

[Kevin Buzzard]

I have manually edited the lakefile.toml so that both mathlib and doc-gen both say rev = "v4.25.0-rc2" and now things have got much further.

[Kevin Buzzard]

@Emily Riehl PR incoming https://github.com/emilyriehl/infinity-cosmos/pull/143

[Kevin Buzzard]

One funny thing about the current main branch of infinity-cosmos is that lean-toolchain says leanprover/lean4:v4.25.0-rc2 but lakefile.toml has mathlib's rev as v4.24.0. Maybe this is the cause of the frustration?

[Arthur Paulino]

Kevin Buzzard said:

Is that wrong? Or right-but-I-am-doomed-to-failure-if-I-bump-rather-than-Pietro?

I think the answer is more nuanced. I'd say "there's no guarantee of success". A Lean dependency carries all of its transitive dependencies with it. Each isolated lib might be tested to build with its locally defined toolchain. But when you add a dependency, you're going to build it with the toolchain explicitly defined in your project.

I forgot what Lake does in case of dependency clashes. I try my absolute best to avoid those. And I never run lake update. Every dependency bump I do is meticulously examined.

[Kevin Buzzard]

Oh but Arthur, all the maths projects just depend on mathlib and nothing else, so we should never get dependency clashes.

[Kevin Buzzard]

Am I right in thinking that this PR here

https://github.com/emilyriehl/infinity-cosmos/pull/142

which was generated by github-actions (presumably a robot) seems to have changed lean-toolchain to v4.25.0-rc2 but left the mathlib dependency in lakefile.lean on v4.24.0? Is that ultimately the cause of the confusion or have I misdiagnosed?

[Arthur Paulino]

And mathlib has its own dependencies. When you bump mathlib, you need to make sure it and all its transitive dependencies actually build with your local toolchain. To be safe, I think it's better to just stick with the toolchain of your mathlib dependency.

[Kevin Buzzard]

Right -- that's exactly what I do with FLT -- every bump is to the most recent commit of mathlib and to whichever version of Lean (and of everything else) that mathlib is using at that time. That's the only thing I ever want to happen. Which is why I'm really hoping it should always be easy.

[Kevin Buzzard]

Does it sound plausible that Emily was sabotaged by a machine with https://github.com/emilyriehl/infinity-cosmos/pull/142 ?

[Kenny Lau]

but you said you tried to bump it independently and got the same error

[Arthur Paulino]

Kevin Buzzard said:

Does it sound plausible that Emily was sabotaged by a machine with https://github.com/emilyriehl/infinity-cosmos/pull/142 ?

It's possible, yes. Looking at the dependencies, some are still on v4.24. The PR bumps the toolchain to v4.25 with seemingly no CI job to check that it builds

[Bryan Gin-ge Chen]

The automation that created the PR is here; it uses leanprover-community/mathlib-update-action, so maybe something can be improved there? cc: @Anne Baanen

I hinted at this in a comment on the PR, but I think for CI to run automatically on those PRs, Emily would have to set up a github token. However, it looks like Emily's repo was created from the pitmonticone/LeanProject template, which doesn't mention that (yet), so it's understandable that she didn't know about this (and quite honestly, we should try to improve things here so that after setting things up once she doesn't have to worry about these sorts of details anymore).

[Anne Baanen]

The action that creates the PRs first runs a lake build on the modified files (you can see that in the logs here). So even though no official green checkmark appears on the PR, it has still been tested.

[Kevin Buzzard]

Looking through those logs I see

Screenshot from 2025-10-29 18-47-34.png

and mathlib commit d9d1cc1012eccfc8d01215b1b7943b0e7f8b7757 is on v4.25.0-rc2. So is it the case that the action checked out a mathlib on v4.25.0-rc2, checked that Emily's repo compiled with it, and then made the PR but neglected to edit lakefile.lean thus leaving the repo itself on mathlib v4.24.0?

[Anne Baanen]

There are two ways you can update your dependencies:

• You just want the freshest commits. In your lakefile.toml you write a branch name, like rev = "master". To update, you run lake update and get to use all the new contributions to Mathlib right now.
• You want to carefully manage your compatibility with specific versions. In your lakefile.toml you write a tag name, like rev = "v4.24.0. To update, you modify lakefile.toml to say rev = "v4.25.0-rc2", then run lake update, and you get that specific version.

The mathlib-update-action, by default, assumes you want to follow the first approach.

[Anne Baanen]

So my advice for using mathlib-update-action would be: do not touch the rev field in your lakefiles, leave it set to rev = "master" and let the machine take care of which updates to apply. :robot:

[Kevin Buzzard]

So for FLT I should change my lakefile.lean to rev = "master" and then complain if anybody ever changes this to something else?

It seems to me that Emily is in a more delicate situation because she is depending on both Mathlib and doc-gen, although I don't really know why infinity-cosmos is any different to FLT.

[Anne Baanen]

Regardless of this advice, mathlib-update-action should absolutely detect when a situation like this occurs and complain. (Unfortunately it is hard to decide whether rev = "v4.24.0" is deliberate or a remnant of a manual update. So we'll have to assume that such a situation means to not upgrade at all, I suppose.)

[Anne Baanen]

Since infinity-cosmos now runs with docgen-action, I suspect we don't actually need to depend on a specific doc-gen revision anymore: the action contains some logic to figure out which doc-gen version is compatible with the current version of Lean.

[Kevin Buzzard]

I'm looking at the history of the lakefile.lean in FLT. I see that at times I even just have

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"

with no rev at all! In fact looking through recent history I see bumps made by people who just seem to be randomly changing the convention from rev = "master" to rev = "v4.whatever" to no rev at all.

[Anne Baanen]

(Removing doc-gen from the Lakefile is not a solution on a larger scale, unfortunately. We'll need to come up with a good versioning scheme across the community, or else suffer through every single Lean package making its own GitHub action to do updates in their preferred way...)

[Kevin Buzzard]

Because I had no real understanding of what was supposed to be happening, I have just let people or machines change the conventions back and forth. My understanding going forwards is that I should stick to rev = "master" and complain if anyone tries to change it.

[Kevin Buzzard]

Thanks for the advice Anne and everyone else! I had never really known what I should be doing here.

[Anne Baanen]

And from my side, apologies for the mess you find yourself in! :sweat_smile:

[Kevin Buzzard]

Aah but there is one dangling question left: what should Emily's lakefile.toml look like?

[Kevin Buzzard]

Right now it has two non-master revs:

name = "InfinityCosmos"
defaultTargets = ["InfinityCosmos"]

[leanOptions]
pp.unicode.fun = true
autoImplicit = false
relaxedAutoImplicit = false

[[require]]
name = "mathlib"
git = "https://github.com/leanprover-community/mathlib4.git"
rev = "v4.25.0-rc2"

[[require]]
name = "checkdecls"
git = "https://github.com/PatrickMassot/checkdecls.git"

[[require]]
name = "«doc-gen4»"
git = "https://github.com/leanprover/doc-gen4"
rev = "v4.25.0-rc2"

[[lean_lib]]
name = "InfinityCosmos"

[Kevin Buzzard]

(oh sorry, that's my PR; right now it has two rev = "v4.24.0"s

[Kevin Buzzard]

I am concerned about doc-gen4 and mathlib using two different versions of lean at the moment a machine bumps.

[Alfredo Moreira-Rosa]

On my side i don't put any rev, and by default it takes whatever is the master branch in any dependencies.

[Kevin Buzzard]

And I am assuming that if you have more than one dependency then you're running a risk here.

[Anne Baanen]

I was about to make a PR to change the lakefile.toml, one moment please :)

[Anne Baanen]

If your project depends on projects A and B, and both depend on Mathlib, then you have a problem, since there is no guaranteed way to update to a version of A and B that use the same version of Mathlib... This needs a social solution, not a technical one unfortunately!

[Ruben Van de Velde]

Yeah, but the social solution is the v4.X tags

[Anne Baanen]

It is certainly part of a solution! Issue is, many projects don't want to wait a month for Mathlib updates.

[Ruben Van de Velde]

Also most projects don't have diamond dependencies on mathlib. I guess right now you need to pick one of the two :)

[Emily Riehl]

Thanks all for looking into this for me. I'm still very confused though!

1. Could you summarize how I should be configuring these files and what I should be doing in the future?
2. Kevin's PR unfortunately broke the blueprint with a very weird error message. It seems to be referring to some stuff I was doing locally in trying to reset up a virtual environment so i could reinstall the leanblueprint command line tools. Or is something else going wrong?
3. The reason I want to bump mathlib was to get the latest version of this file. It's still not there with Kevin's PR. Why not?

[Kevin Buzzard]

Oh dear sorry!

[Anne Baanen]

1. If https://github.com/emilyriehl/infinity-cosmos/pull/144 builds, it should free you from versioning issues. :fingers_crossed: You don't need to modify this file, you can run lake update whenever you want to and commit the resulting lake-manifest.json (or wait for the bot to do so for you).
2. This seems to come from an update in Python, where the pip command removed an option. Let me see if I can fix this for you before my family really get angry at me for not cooking dinner yet :)
3. Kevin bumped Mathlib to v4.25.0-rc2 which is the first version of Mathlib building under Lean version v4.25.0-rc2. After https://github.com/emilyriehl/infinity-cosmos/pull/144 is merged, a simple lake update should give you the latest version of the file.

[Kevin Buzzard]

Yes I see the error I made; "rev=v4.25.0-rc2" is not what you want either in your lakefile.toml; I'm assuming you, like me, are often bumping mathlib because you want the new goodies which have just arrived. I think "rev=master" is what you and I both always want in our lakefile.toml's.

[Anne Baanen]

For 2: thankfully Bryan already fixed this in docgen-action, so updating that action should be enough: https://github.com/emilyriehl/infinity-cosmos/pull/145

[Kevin Buzzard]

Aah -- I can think of a reason why I might want to change lakefile.toml to have rev = "v4.whatever" -- if I want to release versions of FLT corresponding to specific mathlib tags such as v4.whatever. This might help people downstream from me who are having version management issues. However I suspect that the number of people downstream from me is and will remain 0; if someone wants something from FLT then they should be arguing that that thing should be merged into mathlib rather than depending on FLT directly.

[Chris Henson]

I think it is fine to use master during active development if that isn't too much churn for you, but I might suggest pinning a revision once a project is in a "finished" state so that updates past that are more structured.

[Ruben Van de Velde]

Might take a while for FLT :)

[Floris van Doorn]

Anne Baanen said:

There are two ways you can update your dependencies:

• You just want the freshest commits. In your lakefile.toml you write a branch name, like rev = "master". To update, you run lake update and get to use all the new contributions to Mathlib right now.
• You want to carefully manage your compatibility with specific versions. In your lakefile.toml you write a tag name, like rev = "v4.24.0. To update, you modify lakefile.toml to say rev = "v4.25.0-rc2", then run lake update, and you get that specific version.

The mathlib-update-action, by default, assumes you want to follow the first approach.

I think part of the problem is that projects ideally do both:

• stay on master to get the latest Mathlib updates
• once a month make a release against the "stable" Mathlib version (useful for downstream packages and this will show up in the reservoir).

Ideally there should just be a lake exe mk_release (maybe with a lake exe continue_release after fixing all Lean errors) that creates the release on a branch, so that you don't have to ever touch lakefile.toml yourself.

[Ruben Van de Velde]

One could imagine a lake feature where you could update to a specific revision of a dependency regardless of the rev in the lakefile

[Michael Rothgang]

I like the idea of a new lake command! How about lake exe mk_release --continue for the second case?

[Thomas Murrills]

Sebastian Ullrich said:

Alfredo Moreira-Rosa said:

Is the new module behaviour documented somewhere ?

Yes, see https://lean-lang.org/doc/reference/latest/The-Module-System! This is a first documentation draft, now that the system is accessible to users, we will rapidly improve it. So do ask questions.

I have a few questions about the meta phase which I hope are useful to address in the documentation. :) I'm looking at this paragraph:

A meta definition may access (and thus invoke) any meta or non-meta definition of the current module. For accessing imported definitions, the definition must either have been marked as meta when it was declared or the import must be marked as such (meta import when the accessing definition is in the private scope and public meta import otherwise).

1. Does private/public scoping affect meta defs in the same way as it affects regular defs? I.e., the second half of the paragraph indicates that meta defs can itself still be either in the private or public scope, and imported defs which a new meta def invokes must be imported into the correct scope--but then it's a bit confusing that meta defs can access any definition in the current module, regardless of whether it's public or private. I.e. even a public meta def can use a private def from the current module in its body--is that right?
2. Do meta import and public meta import still behave like import and public import as far as the use of non-meta imported defs in new non-meta defs is concerned? (As part of this, does public meta import still put imported public defs in the current module's public scope?)
3. Just to confirm: do meta import all and public meta import all work as you'd expect (i.e. they additionally import private meta defs)?

[Sebastian Ullrich]

Thomas Murrills said:

1. I.e. even a public meta def can use a private def from the current module in its body--is that right?

Yes, same as public def (unless annotated @[expose]). All def rules still apply to meta def.

Do meta import and public meta import still behave like import and public import as far as the use of non-meta imported defs in new non-meta defs is concerned?

I'm not sure I understand this question, if you use meta import, there are no "non-meta imported" defs from that by definition.

(As part of this, does public meta import still put imported public defs in the current module's public scope?)

Yes, they will be public and meta.

Just to confirm: do meta import all and public meta import all work as you'd expect (i.e. they additionally import private meta defs)?

meta import all should. There is no public meta import all just like there is no public import all.

[Thomas Murrills]

Thanks!

Sebastian Ullrich said:

Yes, same as public def (unless annotated @[expose])

Ah, right--still getting used to that. :)

Do meta import and public meta import still behave like import and public import as far as the use of non-meta imported defs in new non-meta defs is concerned?

I'm not sure I understand this question, if you use meta import, there are no "non-meta imported" defs from that by definition.

Sorry, parenthesization ambiguity! I mean "non-meta (imported defs)", i.e. imported defs which were not marked meta when declared, and are now imported. (Though in this context, specifically such defs which have been imported by meta import). :) Going by the public meta import example, it seems the answer is yes!

Sebastian Ullrich said:

meta import all should. There is no public meta import all just like there is no public import all

Oh? The documentation mentions public import all at the bottom of the visibility page! :eyes: Seems like it's treated mostly as syntactic sugar, though, not as a wholly new way to import. (Based on that, I'd expect public meta import all to behave essentially like public meta import followed by meta import all.)

public import all M behaves like public import M followed by import all M, i.e. the all modifier becomes irrelevant for downstream modules.

[Thomas Murrills]

One last question:

If I write public meta import Foo in Bar, thus importing an ordinary, non-meta public def foo in Foo into Bar and marking it both public and meta, does the new meta annotation on foo persist through imports of Bar? I.e., if downstream Baz writes import Bar and gets foo, is foo still meta?

[Sebastian Ullrich]

Yes. Importing declarations acts uniformly independently whether the declaration was defined in the imported module or itself imported into it, so meta is preserved in both cases.

[Sebastian Ullrich]

Thomas Murrills said:

The documentation mentions public import all at the bottom of the visibility page!

Ahh, that information is outdated. Thanks!

[Thomas Murrills]

Ok, thanks! :) Just curious, what's the reasoning behind not having public import all? It does seem like these are independent toggles ("does the imported public scope become private or public" and "is the upstream private scope imported (into the current private scope)"). Is there a technical reason, or is it just that people might think that public import all means "import everything, incl. the private scope, as public"?

[Sebastian Ullrich]

The latter :)

[Robin Carlier]

It seems grind "interactive mode" is now in the latest releases. When can we expect a proper reference manual entry about this?

[František Silváši 🦉]

I've only found this so far :).

[Geoffrey Irving]

I can confirm that leanprover/lean4:v4.26.0-rc1 fixes the recent UInt64 miscompilation bug!

[Chris Henson]

Robin Carlier said:

It seems grind "interactive mode" is now in the latest releases. When can we expect a proper reference manual entry about this?

I'm sure it's in the works, but I would like to second the request for more information about the grind interactive mode, especially anchors. For instance, grind? now uses anchors in the suggestions it makes and it is unclear to me what are the style guidelines are around these.

I think in general (as I mentioned in #mathlib4 > Mathlib: the Missing Manuals @ 💬 ) that it would be helpful to have a style guide entry about grind. One I don't mention there is if grind only is analogous to simp only for squeezing purposes, and I am not sure how grind? suggesting interactive mode fits into that.

[Kim Morrison]

I think it's too early to write style suggestions for grind => in Mathlib. We have to explore how it works for a while.

[Chris Henson]

I mostly meant style suggestions for regular uses of grind, and just a passing mention of grind => because it is already being exposed to users via grind?.

[Kim Morrison]

v4.27.0-rc1 brings many changes to grind:

• allow arbitrary terms as arguments to grind
• better support for Fin n
• congruence closure for function-valued equalities
• renames the cutsat frontend to grind to lia
• support of LawfulOfScientific
• improvements for grind's linarith mode
• many new "guards" for grind_pattern, allowing controlled instantiation (see lean#11429 for docs)
• more aggressive case splitting when non-chronological backtracking is effective
• ... many bug fixes and improvements to corner cases.

[Kim Morrison]

Also of note is significant changes to the behaviour of exact? and apply?:

• exact? falls back to trying "unindexable" theorems if it doesn't otherwise find a result (restoring Lean 3 behaviour). Reports where this is painfully slow in the wild are welcome.
• exact? +all gives all solutions, not just the first one.
• No longer calls solve_by_elim (use try? if you want that behaviour), as exact? is specifically a theorem lookup tool, not a general purpose helper
• exact? +grind calls grind on subsidiary goals. Potentially powerful, and slow. (Reports from the wild very welcome.)

Of particular interest, I would like user reports of places where exact? (possibly with these new options) is effective but painfully slow. I have the machinery in place to add parallelism to exact?, but would like some real world test cases for tuning.

[Kim Morrison]

Finally, between v4.26.0 and v4.27.0 we have added many new features to try? (including, notably, user extensibility via the register_try?_tactic command). It is powerful and often useful, especially in programming applications, and suggestions for further improvements are welcome.

[Wrenna Robson]

Pleased to have two (albeit minor) contributions in this patch :D

[Alfredo Moreira-Rosa]

Same, first minor contribution on my side! (min and max on lists).
Thank you also to Kim and Markus for reviewing it so fast!

[David Loeffler]

So, I just encountered the lia tactic in the wild for the first time, being used to tick off a trivial inequality side condition of the form

k : ℤ
hk : 2 ≤ k
⊢ 0 ≤ k

It's wonderful that we have all these new automation tactics, but I'm a little confused about which ones are preferable for which kinds of goals. Here omega, lia, grind and linarith all work, so which one should be preferred? Or does it not matter?

[Yaël Dillies]

omega and cutsat are both being deprecated to lia. grind uses lia under the hood (and so it is better to use lia directly, to convey what exactly grind is doing). From the name, I suspect linarith might eventually be deprecated to lia too?

[Ruben Van de Velde]

My understanding is that linarith is stronger but also maybe slower? So if lia handles your goal, you probably want to use that

[Ruben Van de Velde]

Docstrings should be updated, though

[Ruben Van de Velde]

(If they haven't already been, I didn't check)

[Ruben Van de Velde]

And do we have a tactic cheat sheet on the community web site by now that needs updating?

[Chris Henson]

Just to clarify, the relationship is that lia (and deprecated cutstat) elaborate into a restricted call to grind, i.e. docs#Lean.Elab.Tactic.evalLia

[Jovan Gerbscheid]

lia only does linear integer arithmetic (hence the name, l.i.a), there it is stronger than linarith. But lia does not handle real inequalities, which linarith does do.

[David Loeffler]

Jovan Gerbscheid said:

lia only does linear integer arithmetic (hence the name, l.i.a), there it is stronger than linarith. But lia does not handle real inequalities, which linarith does do.

I'm slightly puzzled, then, that the following example works:
example (k : ℝ) (hk : 2 ≤ k) : 0 ≤ k := by lia

[Robin Carlier]

it fails when running by lia -order. This is because the "no op config" of grind (here) does not the unset the "order" module.

[Robin Carlier]

(and example (k : Nat) (hk : 2 ≤ k) : 0 ≤ k := by lia -order does work.)

[Chris Henson]

Also #nightly-testing > nightly-testing regression log is relevant, which tracks the extent to which grind/lia can replace omega/ring/linarith/tauto in Mathlib.

[David Loeffler]

I see: so the real-number example is arguably a bug – that the lia tactic is actually doing stuff that it's not meant to.

[David Loeffler]

Shall I make an issue in the lean4 repo for this?

[Kevin Buzzard]

If you make an issue there's a risk they might fix it!

[Kim Morrison]

Yes, that is a bug in lia that I will fix asap.

[Kim Morrison]

linarith and lia are incomparable, as explained above.

[Kim Morrison]

As of quite recently grind is strictly more powerful that linarith (with two known exceptions in mathlib, that I still need to look at). I'm intending to provide a lia style front-end, possibly just called grind_linarith, for users who don't have access to mathlib's linarith (or prefer to avoid it).

[Johan Commelin]

Kim Morrison said:

As of quite recently grind is strictly more powerful that linarith

Can this be made precise? I know that Bhavik and Heather use tactics like linarith as part of proof discovery. Not just as a finishing tactic.
Is it clear that all use cases are covered?

[Kim Morrison]

Johan Commelin said:

Kim Morrison said:

As of quite recently grind is strictly more powerful that linarith

Can this be made precise? I know that Bhavik and Heather use tactics like linarith as part of proof discovery. Not just as a finishing tactic.
Is it clear that all use cases are covered?

What does this mean? linarith closes a goal or fails, just like grind_linarith would.

[Kim Morrison]

When CI completes on https://github.com/leanprover-community/mathlib4-nightly-testing/pull/140 it should hopefully have the few remaining exceptions indicated in the build log.

[Kim Morrison]

Kim Morrison said:

Yes, that is a bug in lia that I will fix asap.

lean#11744, although Mathlib may still need some repair.

[Kim Morrison]

Kim Morrison said:

When CI completes on https://github.com/leanprover-community/mathlib4-nightly-testing/pull/140 it should hopefully have the few remaining exceptions indicated in the build log.

Five files with failures.

• GeckConstruction needs investigating
• Polynomial.Cyclotomic.Eval also
• Combinatorics/Additive/AP/Three/Behrend looks like a grind bug handling arguments; I thought I'd fixed this :woman_shrugging:
• Mathlib.Geometry.Manifold.PartitionOfUnity is the TacticAnalysis framework crashing, perhaps @Anne Baanen might be interested in looking?
• Mathlib.Analysis.SpecialFunctions.Elliptic.Weierstrass is just missing import Mathlib.Data.Rat.Cast.OfScientific. I would really like to get this imported somewhere much lower down, but it has strangely disjoint imports.

[Johan Commelin]

Kim Morrison said:

What does this mean? linarith closes a goal or fails, just like grind_linarith would.

My understanding, from discussing with @Heather Macbeth is that they use linarith's failure in useful ways to discover new proof steps.

[Kim Morrison]

grind also gives witnesses (i.e. a model satisfying all the linear inequalities) when it fails

[Kim Morrison]

(It also does this for integer linear arithmetic, unlike omega.)

[Bhavik Mehta]

For me, I used linear_combination rather than linarith for proof discovery, which was useful to help find slack in inequalities, particularly if I change the discharger it uses.