Zulip Chat Archive

Stream: general

Topic: v4.17.0

Eric Wieser (Mar 03 2025 at 17:07):

Pre-emptively posted before the announcement thread

Since some people may already be running lake update...

As a reminder, please consider updating your packages to the v4.17.0 tag of mathlib before moving on to v4.18.0rc1, as this provides a baseline mathlib version that all projects can be imported with.

Eric Wieser (Mar 03 2025 at 17:13):

You can do this by:

  • making this change to your lakefile.lean:
-require "leanprover-community" / "mathlib" @ git "main"
+require "leanprover-community" / "mathlib" @ git "v4.17.0"

or to your lakefile.toml

 [[require]]
 name = "mathlib"
 scope = "leanprover-community"
+rev = "v4.17.0"
  • lake update mathlib, then fix the build errors
  • git commit -m "Update to Lean 4.17.0", PR, etc
  • git tag v4.17.0 && git push origin v4.17.0
  • Revert the diff to the lakefile above
  • git commit -m "Unpin the lean version", PR, etc

Ruben Van de Velde (Mar 03 2025 at 17:18):

I'm guessing your toml got confused

Shreyas Srinivas (Mar 03 2025 at 18:06):

Eric Wieser said:

As a reminder, please consider updating your packages to the v4.17.0 tag of mathlib before moving on to v4.18.0rc1, as this provides a baseline mathlib version that all projects can be imported with.

I don’t understand. What has changed from before?

Eric Wieser (Mar 03 2025 at 18:07):

Are you asking what is new in v4.17.0? I'll leave that for a release post from the FRO

Shreyas Srinivas (Mar 03 2025 at 18:17):

No I mean, what does it mean that it provides a baseline version of mathlib. I thought all projects with matching toolchains could import mathlib. What has changed?

Shreyas Srinivas (Mar 03 2025 at 18:18):

Is this a bugfix or an incompatibility that causes problems when updating from toolchains < v4.17.0?

Eric Wieser (Mar 03 2025 at 18:20):

I mean a baseline such that someone can write

require "your" / "project" @ "v4.17.0"
require "my" / "work" @ "v4.17.0"

and use theorems from both. It's no use being on the same lean version if you still need different mathlib versions. There is nothing special here about 4.17.0 vs any other version, what is notable is that today is release day and so a good day for this reminder.

Kim Morrison (Mar 03 2025 at 20:56):

I've been think for Mathlib it may be worthwhile to automatically tag master-YYYY-MM-DD every 24 hours, and to have a daily and/or weekly branch that automatically tracks these. (Downstream projects could then require daily or weekly) This would provide more synchronization points if desired.

Eric Wieser (Mar 03 2025 at 21:01):

I think our current problem is not that our synchronization points are too infrequent, but that all our tooling encourages us to skip over them

Eric Wieser (Mar 03 2025 at 21:01):

It took me quite some time to even find the correct spelling for the toml pinning above!

Jireh Loreaux (Mar 03 2025 at 21:19):

Isn't the toml version above wrong?

Eric Wieser (Mar 03 2025 at 21:23):

Wrong in what way?

Jireh Loreaux (Mar 03 2025 at 21:23):

Don't you mean?

+rev = "v4.17.0"

Pietro Monticone (Mar 03 2025 at 21:49):

Or in general: 

+rev = "stable"

Yaël Dillies (Mar 04 2025 at 11:02):

@Kim Morrison, the release notes repeatedly say partial_fixpiont instead of partial_fixpoint

Kim Morrison (Mar 04 2025 at 11:02):

(And we now have some nice automation helping us with the release process itself!)

Kim Morrison (Mar 04 2025 at 11:05):

Yaël Dillies said:

partial_fixpiont

All fixed, thanks.

Last updated: May 02 2025 at 03:31 UTC