Zulip Chat Archive

Stream: new members

Topic: Different import inputs


view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 14:29):

This has nothing to do with the Lean extension to VS Code

view this post on Zulip 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?

view this post on Zulip 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.

view this post on Zulip Nicolò Cavalleri (Jun 29 2020 at 14:31):

Something created with the command leanproject new

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 14:31):

Perfect.

view this post on Zulip 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.

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 14:33):

A screenshot of your VS Code Window seems to be a good start.

view this post on Zulip 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?

view this post on Zulip 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

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 14:35):

If you want two VS Code Windows open then just do "File -> New Window"

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 14:35):

and then "open folder" afterwards

view this post on Zulip Kevin Buzzard (Jun 29 2020 at 14:35):

Are you trying to melt your CPU?

view this post on Zulip 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?

view this post on Zulip Nicolò Cavalleri (Jun 29 2020 at 14:37):

Kevin Buzzard said:

Are you trying to melt your CPU?

Haha it should be fine!

view this post on Zulip 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

view this post on Zulip Nicolò Cavalleri (Jun 29 2020 at 14:39):

Ok the open folder thing solved the problem! Thanks!!

view this post on Zulip 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