Zulip Chat Archive
Stream: new members
Topic: Different import inputs
Nicolò Cavalleri (Jun 29 2020 at 14:28):
I have two different projects and it looks like Lean looks for imports always in the folders of the first (chronologically) project I created. I am trying to look into the settings of the Lean extension of VScode but I cannot find the setting to solve this problem.
Kevin Buzzard (Jun 29 2020 at 14:29):
This has nothing to do with the Lean extension to VS Code
Kevin Buzzard (Jun 29 2020 at 14:29):
A "Lean project" has a very precise meaning. A toml, Lean files in src, etc. Is that what you mean when you talk about your Lean projects?
Kevin Buzzard (Jun 29 2020 at 14:30):
If you do mean this, then using the "open folder" functionality of VS Code and opening the directory which contanis your project will make all your imports work fine.
Nicolò Cavalleri (Jun 29 2020 at 14:31):
Something created with the command leanproject new
Kevin Buzzard (Jun 29 2020 at 14:31):
Perfect.
Kevin Buzzard (Jun 29 2020 at 14:32):
If it doesn't work and you used "open folder" on the root directory of your project, we'll need more precise info.
Kevin Buzzard (Jun 29 2020 at 14:33):
A screenshot of your VS Code Window seems to be a good start.
Nicolò Cavalleri (Jun 29 2020 at 14:33):
Kevin Buzzard said:
If it doesn't work and you used "open folder" on the root directory of your project, we'll need more precise info.
I didn't know I had to use this functionality, I will try now, but it doesn't let me open the two folders simultaneously, do you know if there is a way to do this?
Nicolò Cavalleri (Jun 29 2020 at 14:34):
I mean if I use this functionality and open a new folder it automatically closes the one I had open before
Kevin Buzzard (Jun 29 2020 at 14:35):
If you want two VS Code Windows open then just do "File -> New Window"
Kevin Buzzard (Jun 29 2020 at 14:35):
and then "open folder" afterwards
Kevin Buzzard (Jun 29 2020 at 14:35):
Are you trying to melt your CPU?
Kevin Buzzard (Jun 29 2020 at 14:36):
You want to work on two Lean projects at once, with two VS Code Windows, right? Is that the issue?
Nicolò Cavalleri (Jun 29 2020 at 14:37):
Kevin Buzzard said:
Are you trying to melt your CPU?
Haha it should be fine!
Nicolò Cavalleri (Jun 29 2020 at 14:37):
Kevin Buzzard said:
You want to work on two Lean projects at once, with two VS Code Windows, right? Is that the issue?
Yeah I was trying in the same window but I will use two I guess there's no problem with that
Nicolò Cavalleri (Jun 29 2020 at 14:39):
Ok the open folder thing solved the problem! Thanks!!
Kevin Buzzard (Jun 29 2020 at 14:39):
Oh I see! I don't know if you can do what you want to do, two projects open in one window with it all working properly.
Last updated: Dec 20 2023 at 11:08 UTC