Can Mathlib4 work with lean-auto?

Stream: lean4

[HinaNarukami]

I'm trying to make a project that requires both Mathlib4 and lean-auto, but it turns out to give errors when i tried to compile.
image.png
image.png
It's kinda weird because when I tried to create a complete new project only requiring lean-auto, it does not give any error.
image.png

[Henrik Böving]

Is there a particualr reason you are working with a Lean that's older than a full year here?

[HinaNarukami]

Henrik Böving said:

Is there a particualr reason you are working with a Lean that's older than a full year here?

Just for my researching purpose, and I don't really get what you meant "older than a full year". Can you explain?

[Aaron Liu]

HinaNarukami said:

Henrik Böving said:

Is there a particualr reason you are working with a Lean that's older than a full year here?

Just for my researching purpose, and I don't really get what you meant "older than a full year". Can you explain?

Your Lean release is over a year old (it came out in March 2024).

[Kim Morrison]

It would be great if significant projects which do not depend on mathlib, but are likely to be used with mathlib, included in their CI a step that verifies that they work with mathlib.

(@Johan Commelin, maybe this sort of thing can go on a Mathlib Initiative todo list!)

[HinaNarukami]

Aaron Liu said:

Your Lean release is over a year old (it came out in March 2024).

got it

[HinaNarukami]

Henrik Böving said:

Is there a particualr reason you are working with a Lean that's older than a full year here?

I was using the codes my senior wrote last year, that's why. By the way, I changed the version to 4.21.0 and there's still error.
image.png

[HinaNarukami]

Update: After changing the version, I restart the files, and got this error while building
image.png

[HinaNarukami]

This is the entire error in case anyone is willing to help.
Thank you so much!
Error.txt

[Kim Morrison]

I doubt lean-auto is compatible with that Lean version. You need to find what version it is compatible with.