A question about lean4 installation

Stream: new members

[tsuki]

The following problem occurred when I ran lake build repl
a.png
, does anyone know how to solve it?

[Mauricio Collares]

This probably means the toolchain version specified on the root lean-toolchain file does not match what the repl project expects.

[Mauricio Collares]

You should probably do lake update repl, since the repl project now supports Lean 4.7.0.

[tsuki]

Mauricio Collares said:

You should probably do lake update repl, since the repl project now supports Lean 4.7.0.

c.pngThis command doesn't work :smiling_face_with_tear:

[Mauricio Collares]

You are on an old mathlib as well. Are you sure you want to use Lean 4.7.0? You have two options: Either downgrade lean-toolchain to the version your dependencies expect, or upgrade your dependencies. You can upgrade all of them to the latest version with lake update. Right now this should work because mathlib is still at 4.7.0, but running lake update once mathlib upgrades to 4.8.0-rc1 (once it's released) would probably cause mismatches between repl and mathlib.

[tsuki]

Mauricio Collares said:

You are on an old mathlib as well. Are you sure you want to use Lean 4.7.0? You have two options: Either downgrade lean-toolchain to the version your dependencies expect, or upgrade your dependencies. You can upgrade all of them to the latest version with lake update. Right now this should work because mathlib is still at 4.7.0, but running lake update once mathlib upgrades to 4.8.0-rc1 (once it's released) would probably cause mismatches between repl and mathlib.

Thank you, I have solved this problem successfully！