## 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

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: May 06 2021 at 21:09 UTC