lake update, dont

Stream: ItaLean 2025

[Andrea Carlo Giuseppe Mennucci]

I checked out the git repo for the workshop; I am compiling some code, to learn the basics; when I compile, I see this message:
warning: manifest out of date: git revision of dependency 'mathlib' changed; use lake update mathlib to update it
Advise: do not! if you do, nothing will work afterwards...

[Pietro Monticone]

I’ll pin the rev later today to avoid that message since it might be misleading. Thanks.

[Bhavik Mehta]

https://github.com/pitmonticone/ItaLean2025/pull/117 although I didn't check if it actually works

[Michael Rothgang]

Which version of mathlib will you pin it to? If that's no extra work, can you use a current one?

[Pietro Monticone]

Solving it right now. It's just an obsolete rev. I need to pin the right one. Doing it...

[Pietro Monticone]

Done.

[Pietro Monticone]

Sorry for the inconvenience @Andrea Carlo Giuseppe Mennucci