problem when create new lean project

Stream: new members

[Esteban Estupinan]

Hi all please your help. I m trying to create a new project in Lean, the leanproject new command works, but when I m trying to import for example topology it appears and error "not found in the search path". The project have leanpkg.path and leanpkg.toml files but but it still doesn't work. The project that I want to create is in the location C:\Users\Esteban\Documents\theartofproofLean, Elan folder is in the location C:\Users\Esteban\.elan. What would be the solution for this problem? Or where is the error why the new project is not executed? I attach screenshots. Kind regards

imagen.png
imagen.png
imagen.png

[Richard Hill]

I think this might be because "topology" is a folder in mathlib, not a file. You could try "import topology.basic" (for example) instead.

[Esteban Estupinan]

ok but the error is the same
imagen.png

[Julian Berman]

What are you intending to import, is it indeed the topology.basic file from mathlib? What's in your leanpkg.toml file? And if you run leanproject build what happens?

[Esteban Estupinan]

amm the error is the same
imagen.png

[Esteban Estupinan]

imagen.png

[Julian Berman]

That actually looks like it didn't error, that looks like it succeeded.

If you restart VSCode does that happen to help?

[Esteban Estupinan]

i try it but is the same i believe maybe is a path but i dont know where is the error

[Julian Berman]

Oh wait, that screenshot I think is saying you opened the theartofproofLean folder as your project, but that's not your project, you have to open tablero

[Esteban Estupinan]

Yes open in tablero the errors are done, thank you Julian for your help

[Julian Berman]

Great, glad to hear it.