vscode does not detect mathlib

Stream: new members

[Yvon Fredrich]

Hi,
I tried installing lean by following these tutorials :
https://leanprover-community.github.io/install/windows.html and
https://leanprover-community.github.io/install/project.html
but i get an error (file 'topology\basic' not found in the search path)

Everything is in the screenshot but basically it seems to not find mathlib.
lean --path produces a plausible path
Capture-décran-21.png

By the way, when using VScode I opened the whole project folder (lean_project_1) and not just the src folder.
Also #eval 2+2 works.
Thank you

[Eric Wieser]

What is the content of your leanproject.toml?

[Yvon Fredrich]

leanpkg.toml contains exactly this :

[package]
name = "lean_project_1"
version = "0.1"
lean_version = "leanprover-community/lean:3.50.3"
path = "src"

[dependencies]

(if this is not what you meant I don't know where to find "leanproject.toml")

[Patrick Massot]

Yes, he meant leanpkg.toml. And yours isn't good. How did you create this project? Did you use leanproject new lean_project_1 or something else?

[Yvon Fredrich]

yes I used leanproject new lean_project_1

[Yvon Fredrich]

If it helps, when I create a new project in git bash it looks like this :

yfred@LAPTOP-BMA11Q5D MINGW64 ~/Desktop/LeanPrime
$ leanproject new testpj
Le chemin d’accès spécifié est introuvable.
> cd testpj
> git init -q
> git checkout -b lean-3.50.3
Switched to a new branch 'lean-3.50.3'
configuring testpj 0.1
Command '['leanpkg', 'new', 'testpj']' returned non-zero exit status 1.

"Le chemin d’accès spécifié est introuvable." means "The specified path cannot be found"

[Johan Commelin]

Does leanpkg new testpj return any error messages, besides a non-zero exit status?

[Yvon Fredrich]

No it returns exactly this :

yfred@LAPTOP-BMA11Q5D MINGW64 ~/Desktop/LeanPrime
$ leanpkg new testpj2
Le chemin d’accès spécifié est introuvable.
> cd testpj2
> git init -q
> git checkout -b lean-3.50.3
Switched to a new branch 'lean-3.50.3'
configuring testpj2 0.1