Zulip Chat Archive
Stream: new members
Topic: file import error
Luisitoon (Aug 08 2022 at 14:16):
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 (Aug 08 2022 at 14:22):
Did you open the folder biysc2022 in vscode, rather than any file. I just tried this project and it works for me
Luisitoon (Aug 08 2022 at 14:25):
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 (Aug 08 2022 at 14:39):
You have to use "Open folder..." in vscode and open the root folder named "biysc2022"
Luisitoon (Aug 08 2022 at 14:43):
@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 (Aug 08 2022 at 14:44):
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 (Aug 08 2022 at 14:45):
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 (Aug 08 2022 at 14:48):
Do you mean Ctrl + Shift + N ??
Alex J. Best (Aug 08 2022 at 14:52):
On the command line I just type code some_folder
again and it opens in a different window
Alex J. Best (Aug 08 2022 at 14:53):
But I think ctrl-shift-N does the same
Luisitoon (Aug 08 2022 at 14:55):
Thank you so much, Alex!! You really helped me to make progress!!
Last updated: Dec 20 2023 at 11:08 UTC