downgrading mathlib

Stream: general

[Jelmer Firet]

I want to look at a repository that was last updated in 2018 (https://github.com/awodey/Impredicative , 18th of november 2018 to be exact)
A lot of the imports break because mathlib has changed since then.
How do I use a mathlib version from back then?

[Sebastian Ullrich]

That's Lean 2. What eventually became mathlib was part of core at that point.

[Jelmer Firet]

I have figured out that I can go to an older version of mathlib (leanpkg init, then change rev in leanpkg.toml and run leanproject build)
It still doesn't work and that might be because the project doesn't use mathlib

[Sebastian Ullrich]

Lean 2 predates elan, leanpkg, the VS Code extension, ...