How to add a path exactly

Stream: maths

[Jenny Kim]

Could anyone please help with the following questions:

How to add a path exactly, or how to fix the error that "file 'tactic\suggest' not found in the search path" exactly?

Thanks a lot!

[Alex J. Best]

This should all be handled automatically, which instructions are you following?

[Jenny Kim]

Alex J. Best said:

This should all be handled automatically, which instructions are you following?

I followed https://leanprover-community.github.io/install/windows.html. But why is it not handled automatically? Thanks.

[Junyan Xu]

Did you open the mathlib folder in your editor?

[Kevin Buzzard]

Can you send a screenshot of your VS Code, showing the error and with the file explorer open?

[Kevin Buzzard]

And have you got a correctly configured lean project and are opening the root directory of the project with VS Code's "open folder" functionality?