Help needed: Invalid Import

Stream: lean4

[HinaNarukami]

I'm researching the "Incorrectness Logic", and have cloned the Lean project of the paper. I then ran leanpkg configure, and met this error after the dependencies were installed.
image.png
Does anyone have any idea how to fix it?

[HinaNarukami]

I'm running on WSL btw

[Aaron Liu]

That looks like Lean 3

[Aaron Liu]

I can tell because all the imports are in lowercase

[HinaNarukami]

Yes this is Lean 3
I can't find the stream for Lean 3's topic, that's why i choose Lean 4...

[Aaron Liu]

Lean 3 is deprecated :(

[HinaNarukami]

So basically there's no way I can use this project right?

[František Silváši 🦉]

Normally, Lean 3 projects came with a leanpkg.toml which one could then build with leanpkg build.

[František Silváši 🦉]

But I would strongly discourage you from using Lean 3.

[HinaNarukami]

The reason I try to fix things is because the project used Lean 3.
If there's no way to fix, I may just convert to Lean 4 instead.
Thank you.

[Ruben Van de Velde]

Yeah, if you want to do any more with it than look at the code, you probably should move to lean 4. There's tooling to do that semi-automatically, but I don't know how well it works at this point