Import Error in VS Code

Stream: new members

[Joseph Fletcher]

I followed the setup instructions for Lean found at https://leanprover-community.github.io/install/windows.html and then set up the Mathematics in Lean tutorial. Everything seemed to work fine, but when I open 02_Overview.lean or any other files with imports, I get the error unknown package 'data' in the Lean infoview. I double-checked everything and I don't think I missed any steps. I can see mathlib in the lake-packages folder, so I don't know why it's not working. Can somebody help me out?

[Bulhwi Cha]

Did you clone the mathematics_in_lean repository, not mathematics_in_lean3?

[Marco Campos]

I have also been getting this same error :(

[Marco Campos]

Bulhwi Cha said:

Did you clone the mathematics_in_lean repository, not mathematics_in_lean3?

I installed mathematics_in_lean on a fresh linux machine. Curious, I've seen posts saying that the error is from using Lean3 instead of Lean4 but those commands are in the github repository itself: https://github.com/leanprover-community/mathematics_in_lean/blob/master/MIL/01_Introduction/02_Overview.lean

[Kevin Buzzard]

That is indeed lean 3 code which is presumably erroneously in a lean 4 repository

[Patrick Massot]

Clearly, something went very wrong on our end. I'll investigate immediately.

[Patrick Massot]

I'm really sorry about that mess. The deploying script took old stuff lying around my working copy on this computer. It should be all fixed now.