Error in vscode

Stream: general

[Esteban Martínez Vañó]

Hi everyone.

I'm really new in this world and I have just finished installing lean (in Windows) following the instructions. I've imported the project mathematics_in_lean, but when I open it in vscode I get an error with the import MIL.common.

I've tried changing the terminal directory in vscode but I get the error:
"Imports are out of date and must be rebuilt; use the "Restart File" command in your editor."

If I change the import to "import mathematics_in_lean.MIL.Common" I get the error: "unknown package 'mathematics_in_lean'
You might need to open 'd:\Matemáticas\Universidad\Doctorado\Lean' as a workspace in your editor"

What can I do?

[Asei Inoue]

Hi. please try following steps.

0. use original import statements
1. close vscode, open terminal
2. run lake exe cache get (this may take a long time.)
3. open vscode
4. push "restart file" button

[Julian Berman]

Hello, welcome. The error message at the end there I believe will indicate you've opened d:\Matemáticas\Universidad\Doctorado\Lean but you should be opening wherever you've cloned MIL to -- possibly d:\Matemáticas\Universidad\Doctorado\Lean\mathematics_in_lean? You want to use Open Folder:

Screenshot-2024-07-02-at-12.11.25.png

and the folder you should select is mathematics_in_lean, not the parent folder. The screenshot is macOS obviously but on Windows it should be in the same place.

(Inoue-san's steps possibly also are helpful to review!)

[Esteban Martínez Vañó]

I've tried both suggestion and I get the same errors. When I restart vscode or I press "restar file" it takes a really long time until I get the error again. The problem seems to be with the imports, because I've tried importing other packages and it doesn't work either

[Julian Berman]

Can you show us a screenshot of your VSCode window perhaps? Also when you say import -- are you trying to create some new project which really imports mathematics_in_lean? That I think would be a slightly strange thing to do.

[Julian Berman]

Or are you trying to read mathematics_in_lean itself?

[Esteban Martínez Vañó]

When I say "import" I was refering to the "import" command. I've deleted everything and I'm trying to get mathematics_in_lean again, but this time I've created the folder in disk C (I'm following this page:
https://leanprover-community.github.io/install/project.html
to install it)

[Esteban Martínez Vañó]

If it doesn't work after the new installation I'll post an screenshot

[Esteban Martínez Vañó]

Same error

[Esteban Martínez Vañó]

imagen.png

[Esteban Martínez Vañó]

It's working now! (I don't know why. I've just clicked on "Restart File" again)

[Julian Berman]

Well, glad to hear that at least!