How to work with a specific Mathlib commit

Stream: new members

[Jiatong Yang]

I want to work with a specific Mathlib commit. How should I initialize my project?

[Johan Commelin]

Does the commit have a branch name, or a tag attached to it?

[Johan Commelin]

Otherwise you have to use the commit hash

[Jiatong Yang]

I have the commit hash, but I don't know what to do with my command line.

[Jiatong Yang]

I mean, by following the instructions on Using mathlib4 as a dependency · leanprover-community/mathlib4 Wiki. I will get the newest Mathlib. How can I create a project with the specific commit hash?

[Ruben Van de Velde]

You can do that, look for "master" in your lake file and replace that by your commit hash. Then hopefully lake update will work