file import error

Stream: new members

[Luisitoon]

Hi, I am new on the platform!! I have just got a lean project from "https://github.com/mmasdeu/biysc2022" to run it on VS Code. What I did was, on the terminal: write the comand "leanproject get mmadeu/biysc2022", and everything worked perfectly. However, this project uses some files that the Lean Infoview is not reading. In the code it says "import basic", but file "basic" is not found in the search path, how could I solve this?

[Alex J. Best]

Did you open the folder biysc2022 in vscode, rather than any file. I just tried this project and it works for me

[Luisitoon]

Yes!! For example, I opened the doc "separation.lean" and all is fine except that I am not seeing the goals in the Lean infoview because the file "basic" cannot be imported...

[Alex J. Best]

You have to use "Open folder..." in vscode and open the root folder named "biysc2022"

[Luisitoon]

@Alex J. Best Oh, now I see!! It is working!! The problem was that I had the "Tutorials" Lean project and the "biysc2022" project in the same space...

[Luisitoon]

By the way, is there any way I can have both the Tutorial project and the biysc2022 project in my left side of the VS Code so that I can work with both at the same time??

[Alex J. Best]

I've never seen that, I just open two (or 10) copies of vscode and put them next to each other so I can work on both at once

[Luisitoon]

Do you mean Ctrl + Shift + N ??

[Alex J. Best]

On the command line I just type code some_folder again and it opens in a different window

[Alex J. Best]

But I think ctrl-shift-N does the same

[Luisitoon]

Thank you so much, Alex!! You really helped me to make progress!!