How to pin Mathlib to a specific commit on Lean 4.17?

Stream: mathlib4

[Ceiling Ge]

Hi everyone,

I'm new to Lean 4 and currently using Lean 4.17 (downloaded from the official source). I need to use Mathlib at a specific commit, 8f013c457aea2ea1b0156c0c98043c9ed018529f, but Lean 4.17 keeps pulling in a different Mathlib version automatically. I've tried several approaches—mostly guided by ChatGPT—but none of them have worked, and I'm getting quite confused.

Initially, my lakefile.toml only contained:

[[require]]
name = "mathlib"
scope = "leanprover-community"

Following ChatGPT's advice, I changed it to:

[[require]]
name = "mathlib"
origin = "git"
url = "https://github.com/leanprover-community/mathlib4.git"
rev = "8f013c457aea2ea1b0156c0c98043c9ed018529f"

But running lake update threw an error. I tried a few other suggestions from ChatGPT, which also failed. Then it told me to remove the lakefile.toml and create a lakefile.lean containing:

open Lake DSL

package «2025-02-24_try»

require mathlib from git
  "https://github.com/leanprover-community/mathlib4.git"
  @ "8f013c457aea2ea1b0156c0c98043c9ed018529f"

However, after doing so, I ran into even more errors, particularly involving proofwidgets:

  inputFile (widgetDir / { toString := "package.json" })
has type
  Bool → SpawnM (Job FilePath)
but is expected to have type
  FetchM ?m.644
...
error: package configuration has errors

Now I'm stuck and not sure how to proceed. Any help on how to properly pin Mathlib to the 8f013c457... commit in Lean 4.17 without running into these errors would be greatly appreciated! :star_struck:

[Patrick Massot]

In the toml version

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

should work

[Patrick Massot]

See https://lean-lang.org/doc/reference/latest/Build-Tools-and-Distribution/Lake/#The-Lean-Language-Reference--Build-Tools-and-Distribution--Lake--Configuration-File-Format--Declarative-TOML-Format--Dependencies

[Eric Wieser]

That commit requires Lean 4.5.0-rc1, not 4.17.0 : https://github.com/leanprover-community/mathlib4/blob/8f013c457aea2ea1b0156c0c98043c9ed018529f/lean-toolchain

[Patrick Massot]

@David Thrane Christiansen I built the above url by inspecting the id of that section. Is there a better way?

[Eric Wieser]

You can't pick and choose your Lean and mathlib version separately, and if you use elan it solves these problems for you

[Patrick Massot]

I think that pinning the mathlib commit and using lake update will set the correct Lean version for the project.

[Eric Wieser]

My understanding from "downloaded from the official source)" is that @Ceiling Ge has opted to install Lean manually and not use elan, assuming I am not confusing them with another recent poster. (edit: I am)

[Patrick Massot]

Oh I see. Then they are on their own I guess.

[Eric Wieser]

But also, I'd be surprised if lake update has two years of backwards compatibility

[Patrick Massot]

I’d be surprised if it had two months of backward compatibility.

[Ceiling Ge]

Thank you all @Eric Wieser @Patrick Massot so much for your quick and detailed help! This was my first time asking a question here, and I’m really touched by how responsive everyone is. I followed your advice (installed elan, pinned Mathlib properly, etc.) and now everything is working great. I’ll keep learning Lean 4, and hopefully one day I can pay it forward and help others the way you helped me. Wishing you all the best! :grinning:

[David Thrane Christiansen]

Patrick Massot said:

David Thrane Christiansen I built the above url by inspecting the id of that section. Is there a better way?

In general, yes - right now, not for that one.

Over many of the page elements, including but not limited to headers, hovering gets you a little floating link icon from which you can copy a permalink that will be stable across manual revisions, even as content is reorganized. This section hasn't been assigned one yet, but it will get one soon.

For an example of what this looks like, see e.g. Functor. This link will keep working as long as there's documentation for something called Functor, no matter where in the book it is.

[Eric Wieser]

Does this mean that there is a mechanism to prevent the same thing being included into multiple documents?

[David Thrane Christiansen]

There is not. Once cross-document cross-references get implemented, links will link to the current document by default, or to another one if explicitly specified.

[Eric Wieser]

What does the link above do if there are multiple matches?

[David Thrane Christiansen]

There's two components in it: a "domain" that's like a domain of discourse, and a specific item in that domain. Each item in the domain is mapped to a set of locations that document it in an internal table. Right now, the permalink mechanism only generates the link if that set is a singleton. Eventually, for most domains, it'll become a documentation-build-time error that can be disabled.

[David Thrane Christiansen]

If you're writing Verso code that uses this feature, you can also do things like allowing a local override of the name used for a documentation item to allow two separate permalinks

[David Thrane Christiansen]

Or require that they be specified manually - that's why some sections in the reference don't yet have permalinks, because manually naming them ensures that they have a stable identity that can be preserved across revisions