How to configure Mathlib version for earlier Lean version?

Stream: new members

[mars0i]

It appears that when I require Mathlib in the simplest way possible, with this in lakefile.lean,

lean_lib «ChaosLean» where
  require mathlib from git "https://github.com/leanprover-community/mathlib4"

lake update then overwrites lean-toolchain to use the most recent version of Lean:

info: updating toolchain to 'leanprover/lean4:v4.15.0-rc1'

and indeed, the contents of lean-toolchain has been changed to

leanprover/lean4:v4.15.0-rc1

How can I use an earlier version of Lean with Mathlib, in particular the latest stable release, v4.14.0? I assume that what's happening is that the simple require line causes lake update to get the latest version of Mathlib, which is only compatible with the latest version of Lean. I'm guessing that there's something I need to change the require line to cause it use a version of Mathlib that's compatible with 4.14.0. Or maybe I need to add arguments to lake update? (Why? I'm trying to debug a problem, and wondering whether 4.15.0-rc1 is causing it.)

(As an aside, as a newbie and thus still an outsider, this feels like a bad practice: the standard configuration practice overwrites the user's chosen configuration, and in addition forces them to use a release candidate rather than the latest stable release. Lean developers and Mathlib contributors might want that, but other users might not.)

[Ruben Van de Velde]

You're asking for the latest version of mathlib - there's only one version of lean that works with that

[Ruben Van de Velde]

Try

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

[mars0i]

Thanks @Ruben Van de Velde!